--- a/NEWS Wed Sep 29 17:58:27 2010 +0200
+++ b/NEWS Wed Sep 29 17:59:20 2010 +0200
@@ -74,10 +74,12 @@
*** HOL ***
+* Dropped old primrec package. INCOMPATIBILITY.
+
* Improved infrastructure for term evaluation using code generator
techniques, in particular static evaluation conversions.
-* String.literal is a type, but not a datatype. INCOMPATIBILITY.
+* String.literal is a type, but not a datatype. INCOMPATIBILITY.
* Renamed lemmas:
expand_fun_eq -> fun_eq_iff
@@ -236,6 +238,9 @@
generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
The theorems bij_def and surj_def are unchanged.
+* Function package: .psimps rules are no longer implicitly declared [simp].
+INCOMPATIBILITY.
+
*** FOL ***
* All constant names are now qualified. INCOMPATIBILITY.
--- a/doc-src/Classes/IsaMakefile Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Classes/IsaMakefile Wed Sep 29 17:59:20 2010 +0200
@@ -23,10 +23,10 @@
Thy: $(THY)
-$(THY): Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
+$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML
@$(USEDIR) HOL Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
- Thy/document/pdfsetup.sty Thy/document/session.tex
+ Thy/document/pdfsetup.sty Thy/document/session.tex
## clean
--- a/doc-src/Classes/Thy/Classes.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Wed Sep 29 17:59:20 2010 +0200
@@ -601,14 +601,14 @@
\noindent This maps to Haskell as follows:
*}
(*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (Haskell)}
*}
text {*
\noindent The code in SML has explicit dictionary passing:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (SML)}
*}
@@ -617,7 +617,7 @@
\noindent In Scala, implicts are used as dictionaries:
*}
(*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (Scala)}
*}
--- a/doc-src/Classes/Thy/document/Classes.tex Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Sep 29 17:59:20 2010 +0200
@@ -1123,11 +1123,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -1195,23 +1195,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The code in SML has explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -1295,12 +1295,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent In Scala, implicts are used as dictionaries:%
@@ -1320,11 +1320,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
object\ Example\ {\isacharbraceleft}\isanewline
@@ -1398,12 +1398,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Inspecting the type class universe%
}
--- a/doc-src/Classes/style.sty Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Classes/style.sty Wed Sep 29 17:59:20 2010 +0200
@@ -28,14 +28,16 @@
\newcommand{\quotebreak}{\\[1.2ex]}
%% typewriter text
-\isakeeptag{typewriter}
\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
\renewcommand{\isadigit}[1]{{##1}}%
\parindent0pt%
+\makeatletter\isa@parindent0pt\makeatother%
\isabellestyle{tt}\isastyle%
\fontsize{9pt}{9pt}\selectfont}{}
-\renewcommand{\isatagtypewriter}{\begin{typewriter}}
-\renewcommand{\endisatagtypewriter}{\end{typewriter}}
+
+\isakeeptag{quotetypewriter}
+\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
+\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
--- a/doc-src/Codegen/IsaMakefile Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/IsaMakefile Wed Sep 29 17:59:20 2010 +0200
@@ -23,7 +23,7 @@
Thy: $(THY)
-$(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
+$(THY): $(OUT)/HOL-Library Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
@$(USEDIR) -m no_brackets -m iff HOL-Library Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
--- a/doc-src/Codegen/Thy/Adaptation.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed Sep 29 17:59:20 2010 +0200
@@ -175,7 +175,7 @@
code_const %invisible True and False and "op \<and>" and Not
(SML and and and)
(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts in_interval (SML)}
*}
@@ -190,9 +190,9 @@
"bool"}, we may use \qn{custom serialisations}:
*}
-code_type %quote %tt bool
+code_type %quotett bool
(SML "bool")
-code_const %quote %tt True and False and "op \<and>"
+code_const %quotett True and False and "op \<and>"
(SML "true" and "false" and "_ andalso _")
text {*
@@ -206,7 +206,7 @@
placeholder for the type constructor's (the constant's) arguments.
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts in_interval (SML)}
*}
@@ -218,10 +218,10 @@
precedences which may be used here:
*}
-code_const %quote %tt "op \<and>"
+code_const %quotett "op \<and>"
(SML infixl 1 "andalso")
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts in_interval (SML)}
*}
@@ -247,9 +247,9 @@
code_const %invisible Pair
(SML)
(*>*)
-code_type %quote %tt prod
+code_type %quotett prod
(SML infix 2 "*")
-code_const %quote %tt Pair
+code_const %quotett Pair
(SML "!((_),/ (_))")
text {*
@@ -283,10 +283,10 @@
@{command_def code_class}) and its operation @{const [source] HOL.equal}
*}
-code_class %quote %tt equal
+code_class %quotett equal
(Haskell "Eq")
-code_const %quote %tt "HOL.equal"
+code_const %quotett "HOL.equal"
(Haskell infixl 4 "==")
text {*
@@ -307,7 +307,7 @@
end %quote (*<*)
-(*>*) code_type %quote %tt bar
+(*>*) code_type %quotett bar
(Haskell "Integer")
text {*
@@ -316,7 +316,7 @@
suppress this additional instance, use @{command_def "code_instance"}:
*}
-code_instance %quote %tt bar :: equal
+code_instance %quotett bar :: equal
(Haskell -)
@@ -328,10 +328,10 @@
"code_include"} command:
*}
-code_include %quote %tt Haskell "Errno"
+code_include %quotett Haskell "Errno"
{*errno i = error ("Error number: " ++ show i)*}
-code_reserved %quote %tt Haskell Errno
+code_reserved %quotett Haskell Errno
text {*
\noindent Such named @{text include}s are then prepended to every
--- a/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy Wed Sep 29 17:59:20 2010 +0200
@@ -206,7 +206,7 @@
datatype %quote form = T | F | And form form | Or form form (*<*)
-(*>*) ML %tt %quote {*
+(*>*) ML %quotett {*
fun eval_form @{code T} = true
| eval_form @{code F} = false
| eval_form (@{code And} (p, q)) =
--- a/doc-src/Codegen/Thy/Foundations.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Wed Sep 29 17:59:20 2010 +0200
@@ -161,7 +161,7 @@
is determined syntactically. The resulting code:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts dequeue (consts) dequeue (Haskell)}
*}
@@ -217,7 +217,7 @@
equality check, as can be seen in the corresponding @{text SML} code:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts collect_duplicates (SML)}
*}
@@ -255,7 +255,7 @@
for the pattern @{term "AQueue [] []"}:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
*}
@@ -296,7 +296,7 @@
exception at the appropriate position:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
*}
--- a/doc-src/Codegen/Thy/Further.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Wed Sep 29 17:59:20 2010 +0200
@@ -112,7 +112,7 @@
After this setup procedure, code generation can continue as usual:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
*}
--- a/doc-src/Codegen/Thy/Introduction.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Sep 29 17:59:20 2010 +0200
@@ -70,7 +70,7 @@
text {* \noindent resulting in the following code: *}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts empty enqueue dequeue (SML)}
*}
@@ -93,7 +93,7 @@
\noindent This is the corresponding code:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts empty enqueue dequeue (Haskell)}
*}
@@ -168,7 +168,7 @@
native classes:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts bexp (Haskell)}
*}
@@ -178,7 +178,7 @@
@{text SML}:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts bexp (SML)}
*}
--- a/doc-src/Codegen/Thy/Refinement.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Wed Sep 29 17:59:20 2010 +0200
@@ -31,7 +31,7 @@
to two recursive calls:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts fib (consts) fib (Haskell)}
*}
@@ -69,7 +69,7 @@
\noindent The resulting code shows only linear growth of runtime:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts fib (consts) fib fib_step (Haskell)}
*}
@@ -157,7 +157,7 @@
\noindent The resulting code looks as expected:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts empty enqueue dequeue (SML)}
*}
@@ -253,7 +253,7 @@
\noindent Then the corresponding code is as follows:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
*} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Sep 29 17:59:20 2010 +0200
@@ -228,11 +228,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -264,12 +264,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent Though this is correct code, it is a little bit
@@ -281,23 +281,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bool\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} command takes a type constructor
@@ -311,11 +311,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -338,12 +338,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent This still is not perfect: the parentheses around the
@@ -354,26 +354,26 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -396,12 +396,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The attentive reader may ask how we assert that no
@@ -447,23 +447,23 @@
%
\endisadeliminvisible
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ prod\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ Pair\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The initial bang ``\verb|!|'' tells the serialiser
@@ -499,11 +499,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
\ equal\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -511,12 +511,12 @@
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}HOL{\isachardot}equal{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent A problem now occurs whenever a type which is an instance
@@ -553,20 +553,20 @@
%
\endisadelimquote
%
-\isadelimtt
+\isadelimquotett
\ %
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bar\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The code generator would produce an additional instance,
@@ -575,20 +575,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
\ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline
\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
}
@@ -600,23 +600,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}include}\isamarkupfalse%
\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
\isanewline
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
\ Haskell\ Errno%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent Such named \isa{include}s are then prepended to every
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Wed Sep 29 17:59:20 2010 +0200
@@ -269,7 +269,20 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadelimquotett
+\ %
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{ML}\isamarkupfalse%
\ {\isacharverbatimopen}\isanewline
\ \ fun\ eval{\isacharunderscore}form\ %
\isaantiq
@@ -294,12 +307,12 @@
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
-\endisatagquote
-{\isafoldquote}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimquote
+\isadelimquotett
%
-\endisadelimquote
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent \isa{code} takes as argument the name of a constant;
--- a/doc-src/Codegen/Thy/document/Foundations.tex Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Wed Sep 29 17:59:20 2010 +0200
@@ -238,11 +238,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -253,12 +253,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has
@@ -338,11 +338,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -373,12 +373,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent Obviously, polymorphic equality is implemented the Haskell
@@ -431,11 +431,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -447,12 +447,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent In some cases it is desirable to have this
@@ -520,11 +520,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline
@@ -538,12 +538,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent This feature however is rarely needed in practice. Note
--- a/doc-src/Codegen/Thy/document/Further.tex Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Sep 29 17:59:20 2010 +0200
@@ -207,11 +207,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
@@ -224,12 +224,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Imperative data structures%
}
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Sep 29 17:59:20 2010 +0200
@@ -133,11 +133,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -176,12 +176,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
@@ -216,11 +216,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -245,12 +245,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see
@@ -382,11 +382,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -431,12 +431,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent This is a convenient place to show how explicit dictionary
@@ -445,11 +445,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -499,12 +499,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Wed Sep 29 17:59:20 2010 +0200
@@ -65,11 +65,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
@@ -79,12 +79,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent A more efficient implementation would use dynamic
@@ -161,11 +161,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -180,12 +180,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Datatype refinement%
}
@@ -337,11 +337,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -380,12 +380,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
The same techniques can also be applied to types which are not
@@ -571,11 +571,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -609,12 +609,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
Typical data structures implemented by representations involving
--- a/doc-src/Codegen/style.sty Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Codegen/style.sty Wed Sep 29 17:59:20 2010 +0200
@@ -28,17 +28,20 @@
\newcommand{\quotebreak}{\\[1.2ex]}
%% typewriter text
-\isakeeptag{typewriter}
\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
\renewcommand{\isadigit}[1]{{##1}}%
\parindent0pt%
+\makeatletter\isa@parindent0pt\makeatother%
\isabellestyle{tt}\isastyle%
\fontsize{9pt}{9pt}\selectfont}{}
-\renewcommand{\isatagtypewriter}{\begin{typewriter}}
-\renewcommand{\endisatagtypewriter}{\end{typewriter}}
-\isakeeptag{tt}
-\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
+\isakeeptag{quotetypewriter}
+\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
+\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
+
+\isakeeptag{quotett}
+\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quote}}
%% a trick
\newcommand{\isasymSML}{SML}
--- a/doc-src/Functions/IsaMakefile Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Functions/IsaMakefile Wed Sep 29 17:59:20 2010 +0200
@@ -23,7 +23,7 @@
Thy: $(THY)
-$(THY): Thy/ROOT.ML Thy/Functions.thy
+$(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Functions.thy
@$(USEDIR) HOL Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
--- a/doc-src/Functions/Thy/Functions.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/doc-src/Functions/Thy/Functions.thy Wed Sep 29 17:59:20 2010 +0200
@@ -580,7 +580,6 @@
| "fib2 1 = 1"
| "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
-(*<*)ML_val "goals_limit := 1"(*>*)
txt {*
This kind of matching is again justified by the proof of pattern
completeness and compatibility.
@@ -588,7 +587,7 @@
either @{term "0::nat"}, @{term "1::nat"} or @{term "n +
(2::nat)"}:
- @{subgoals[display,indent=0]}
+ @{subgoals[display,indent=0,goals_limit=1]}
This is an arithmetic triviality, but unfortunately the
@{text arith} method cannot handle this specific form of an
@@ -597,7 +596,6 @@
existentials, which can then be solved by the arithmetic decision procedure.
Pattern compatibility and termination are automatic as usual.
*}
-(*<*)ML_val "goals_limit := 10"(*>*)
apply atomize_elim
apply arith
apply auto
@@ -765,11 +763,10 @@
\noindent The hypothesis in our lemma was used to satisfy the first premise in
the induction rule. However, we also get @{term
"findzero_dom (f, n)"} as a local assumption in the induction step. This
- allows to unfold @{term "findzero f n"} using the @{text psimps}
- rule, and the rest is trivial. Since the @{text psimps} rules carry the
- @{text "[simp]"} attribute by default, we just need a single step:
+ allows unfolding @{term "findzero f n"} using the @{text psimps}
+ rule, and the rest is trivial.
*}
-apply simp
+apply (simp add: findzero.psimps)
done
text {*
@@ -796,7 +793,7 @@
have "f n \<noteq> 0"
proof
assume "f n = 0"
- with dom have "findzero f n = n" by simp
+ with dom have "findzero f n = n" by (simp add: findzero.psimps)
with x_range show False by auto
qed
@@ -807,7 +804,7 @@
with `f n \<noteq> 0` show ?thesis by simp
next
assume "x \<in> {Suc n ..< findzero f n}"
- with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp
+ with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by (simp add: findzero.psimps)
with IH and `f n \<noteq> 0`
show ?thesis by simp
qed
@@ -1071,7 +1068,7 @@
*}
(*<*)oops(*>*)
lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
- by (induct rule:nz.pinduct) auto
+ by (induct rule:nz.pinduct) (auto simp: nz.psimps)
text {*
We formulate this as a partial correctness lemma with the condition
@@ -1107,7 +1104,7 @@
lemma f91_estimate:
assumes trm: "f91_dom n"
shows "n < f91 n + 11"
-using trm by induct auto
+using trm by induct (auto simp: f91.psimps)
termination
proof
--- a/src/FOL/hypsubstdata.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/FOL/hypsubstdata.ML Wed Sep 29 17:59:20 2010 +0200
@@ -13,8 +13,6 @@
val subst = @{thm subst}
val sym = @{thm sym}
val thin_refl = @{thm thin_refl}
- val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
- by (unfold prop_def) (drule eq_reflection, unfold)}
end;
structure Hypsubst = HypsubstFun(Hypsubst_Data);
--- a/src/HOL/HOL.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/HOL.thy Wed Sep 29 17:59:20 2010 +0200
@@ -834,8 +834,6 @@
val subst = @{thm subst}
val sym = @{thm sym}
val thin_refl = @{thm thin_refl};
- val prop_subst = @{lemma "PROP P t ==> PROP prop (x = t ==> PROP P x)"
- by (unfold prop_def) (drule eq_reflection, unfold)}
end);
open Hypsubst;
--- a/src/HOL/Imperative_HOL/Mrec.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy Wed Sep 29 17:59:20 2010 +0200
@@ -54,7 +54,7 @@
| None \<Rightarrow> None)
| None \<Rightarrow> None
)"
-apply (cases "mrec_dom (x,h)", simp)
+apply (cases "mrec_dom (x,h)", simp add: mrec.psimps)
apply (frule mrec_default)
apply (frule mrec_di_reverse, simp)
by (auto split: sum.split option.split simp: mrec_default)
@@ -105,7 +105,7 @@
proof (cases a)
case (Inl aa)
from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
- by auto
+ by (auto simp: mrec.psimps)
next
case (Inr b)
note Inr' = this
@@ -122,15 +122,15 @@
apply auto
apply (rule rec_case)
apply auto
- unfolding MREC_def by auto
+ unfolding MREC_def by (auto simp: mrec.psimps)
next
case None
- from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
+ from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps)
qed
qed
next
case None
- from this 1(1) mrec 1(3) show ?thesis by simp
+ from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps)
qed
qed
from this h'_r show ?thesis by simp
--- a/src/HOL/Inductive.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Inductive.thy Wed Sep 29 17:59:20 2010 +0200
@@ -14,7 +14,6 @@
"Tools/Datatype/datatype_case.ML"
("Tools/Datatype/datatype_abs_proofs.ML")
("Tools/Datatype/datatype_data.ML")
- ("Tools/old_primrec.ML")
("Tools/primrec.ML")
("Tools/Datatype/datatype_codegen.ML")
begin
@@ -282,7 +281,6 @@
use "Tools/Datatype/datatype_codegen.ML"
setup Datatype_Codegen.setup
-use "Tools/old_primrec.ML"
use "Tools/primrec.ML"
text{* Lambda-abstractions with pattern matching: *}
--- a/src/HOL/IsaMakefile Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 29 17:59:20 2010 +0200
@@ -202,7 +202,6 @@
Tools/inductive_set.ML \
Tools/lin_arith.ML \
Tools/nat_arith.ML \
- Tools/old_primrec.ML \
Tools/primrec.ML \
Tools/prop_logic.ML \
Tools/refute.ML \
@@ -1053,7 +1052,7 @@
SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \
SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \
SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \
- SET_Protocol/document/root.tex
+ SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
@@ -1176,6 +1175,7 @@
Nominal/nominal_permeq.ML \
Nominal/nominal_primrec.ML \
Nominal/nominal_thmdecls.ML \
+ Nominal/old_primrec.ML \
Library/Infinite_Set.thy
@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
--- a/src/HOL/Library/Code_Natural.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Wed Sep 29 17:59:20 2010 +0200
@@ -78,7 +78,7 @@
def equals(that: Natural): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
- def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
+ def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
this.value.intValue
else error("Int value out of range: " + this.value.toString)
--- a/src/HOL/Library/Efficient_Nat.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Sep 29 17:59:20 2010 +0200
@@ -303,7 +303,7 @@
def equals(that: Nat): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
- def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
+ def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
this.value.intValue
else error("Int value out of range: " + this.value.toString)
--- a/src/HOL/Library/Kleene_Algebra.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy Wed Sep 29 17:59:20 2010 +0200
@@ -483,56 +483,4 @@
end
-subsection {* A naive algorithm to generate the transitive closure *}
-
-function (default "\<lambda>x. 0", tailrec, domintros)
- mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
-where
- "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
- by pat_completeness simp
-
-declare mk_tcl.simps[simp del] (* loops *)
-
-lemma mk_tcl_code[code]:
- "mk_tcl A X =
- (let XA = X * A
- in if XA \<le> X then X else mk_tcl A (X + XA))"
- unfolding mk_tcl.simps[of A X] Let_def ..
-
-context kleene
-begin
-
-lemma mk_tcl_lemma1: "(X + X * A) * star A = X * star A"
-by (metis ka1 left_distrib mult_assoc mult_left_mono ord_simp2 zero_minimum)
-
-lemma mk_tcl_lemma2: "X * A \<le> X \<Longrightarrow> X * star A = X"
-by (rule antisym) (auto simp: star4)
-
end
-
-lemma mk_tcl_correctness:
- fixes X :: "'a::kleene"
- assumes "mk_tcl_dom (A, X)"
- shows "mk_tcl A X = X * star A"
- using assms
- by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2)
-
-lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
- by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
-
-lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
- unfolding mk_tcl_def
- by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
-
-text {* We can replace the dom-Condition of the correctness theorem
- with something executable: *}
-
-lemma mk_tcl_correctness2:
- fixes A X :: "'a :: {kleene}"
- assumes "mk_tcl A A \<noteq> 0"
- shows "mk_tcl A A = tcl A"
- using assms mk_tcl_default mk_tcl_correctness
- unfolding tcl_def
- by auto
-
-end
--- a/src/HOL/Library/More_List.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Library/More_List.thy Wed Sep 29 17:59:20 2010 +0200
@@ -16,7 +16,6 @@
declare (in linorder) Max_fin_set_fold [code_unfold del]
declare (in complete_lattice) Inf_set_fold [code_unfold del]
declare (in complete_lattice) Sup_set_fold [code_unfold del]
-declare rev_foldl_cons [code del]
text {* Fold combinator with canonical argument order *}
@@ -101,11 +100,13 @@
"fold plus xs = plus (listsum (rev xs))"
by (induct xs) (simp_all add: add.assoc)
-lemma listsum_conv_foldr [code]:
- "listsum xs = foldr plus xs 0"
- by (fact listsum_foldr)
+declare listsum_foldl [code del]
-lemma sort_key_conv_fold:
+lemma (in monoid_add) listsum_conv_fold [code]:
+ "listsum xs = fold (\<lambda>x y. y + x) xs 0"
+ by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
+
+lemma (in linorder) sort_key_conv_fold:
assumes "inj_on f (set xs)"
shows "sort_key f xs = fold (insort_key f) xs []"
proof -
@@ -115,13 +116,14 @@
fix x y
assume "x \<in> set xs" "y \<in> set xs"
with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
+ have **: "x = y \<longleftrightarrow> y = x" by auto
show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
- by (induct zs) (auto dest: *)
+ by (induct zs) (auto intro: * simp add: **)
qed
then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
qed
-lemma sort_conv_fold:
+lemma (in linorder) sort_conv_fold:
"sort xs = fold insort xs []"
by (rule sort_key_conv_fold) simp
--- a/src/HOL/List.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/List.thy Wed Sep 29 17:59:20 2010 +0200
@@ -94,10 +94,9 @@
"concat [] = []"
| "concat (x # xs) = x @ concat xs"
-primrec (in monoid_add)
+definition (in monoid_add)
listsum :: "'a list \<Rightarrow> 'a" where
- "listsum [] = 0"
- | "listsum (x # xs) = x + listsum xs"
+ "listsum xs = foldr plus xs 0"
primrec
drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -261,7 +260,7 @@
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\
@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\
-@{lemma "listsum [1,2,3::nat] = 6" by simp}
+@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
\end{tabular}}
\caption{Characteristic examples}
\label{fig:Characteristic}
@@ -2369,27 +2368,30 @@
qed
+text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
+
+lemma foldr_foldl:
+ "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
+ by (induct xs) auto
+
+lemma foldl_foldr:
+ "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
+ by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
+
+
text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
-lemma foldl_foldr1_lemma:
- "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
-by (induct xs arbitrary: a) (auto simp:add_assoc)
-
-corollary foldl_foldr1:
- "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
-by (simp add:foldl_foldr1_lemma)
-
-
-text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
-
-lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
-by (induct xs) auto
-
-lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
-by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
-
-lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
- by (induct xs, auto simp add: foldl_assoc add_commute)
+lemma (in monoid_add) foldl_foldr1_lemma:
+ "foldl op + a xs = a + foldr op + xs 0"
+ by (induct xs arbitrary: a) (auto simp: add_assoc)
+
+corollary (in monoid_add) foldl_foldr1:
+ "foldl op + 0 xs = foldr op + xs 0"
+ by (simp add: foldl_foldr1_lemma)
+
+lemma (in ab_semigroup_add) foldr_conv_foldl:
+ "foldr op + xs a = foldl op + a xs"
+ by (induct xs) (simp_all add: foldl_assoc add.commute)
text {*
Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
@@ -2869,56 +2871,57 @@
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
-lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
-by (induct xs) (simp_all add:add_assoc)
-
-lemma listsum_rev [simp]:
- fixes xs :: "'a\<Colon>comm_monoid_add list"
- shows "listsum (rev xs) = listsum xs"
-by (induct xs) (simp_all add:add_ac)
-
-lemma listsum_map_remove1:
-fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
-shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
-by (induct xs)(auto simp add:add_ac)
-
-lemma list_size_conv_listsum:
+lemma (in monoid_add) listsum_foldl [code]:
+ "listsum = foldl (op +) 0"
+ by (simp add: listsum_def foldl_foldr1 fun_eq_iff)
+
+lemma (in monoid_add) listsum_simps [simp]:
+ "listsum [] = 0"
+ "listsum (x#xs) = x + listsum xs"
+ by (simp_all add: listsum_def)
+
+lemma (in monoid_add) listsum_append [simp]:
+ "listsum (xs @ ys) = listsum xs + listsum ys"
+ by (induct xs) (simp_all add: add.assoc)
+
+lemma (in comm_monoid_add) listsum_rev [simp]:
+ "listsum (rev xs) = listsum xs"
+ by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute)
+
+lemma (in comm_monoid_add) listsum_map_remove1:
+ "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
+ by (induct xs) (auto simp add: ac_simps)
+
+lemma (in monoid_add) list_size_conv_listsum:
"list_size f xs = listsum (map f xs) + size xs"
-by(induct xs) auto
-
-lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
-by (induct xs) auto
-
-lemma length_concat: "length (concat xss) = listsum (map length xss)"
-by (induct xss) simp_all
-
-lemma listsum_map_filter:
- fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
- assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
+ by (induct xs) auto
+
+lemma (in monoid_add) length_concat:
+ "length (concat xss) = listsum (map length xss)"
+ by (induct xss) simp_all
+
+lemma (in monoid_add) listsum_map_filter:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
shows "listsum (map f (filter P xs)) = listsum (map f xs)"
-using assms by (induct xs) auto
-
-text{* For efficient code generation ---
- @{const listsum} is not tail recursive but @{const foldl} is. *}
-lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
-by(simp add:listsum_foldr foldl_foldr1)
-
-lemma distinct_listsum_conv_Setsum:
- "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
-by (induct xs) simp_all
-
-lemma listsum_eq_0_nat_iff_nat[simp]:
- "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
-by(simp add: listsum)
-
-lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
+ using assms by (induct xs) auto
+
+lemma (in monoid_add) distinct_listsum_conv_Setsum:
+ "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
+ by (induct xs) simp_all
+
+lemma listsum_eq_0_nat_iff_nat [simp]:
+ "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
+ by (simp add: listsum_foldl)
+
+lemma elem_le_listsum_nat:
+ "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
apply(induct ns arbitrary: k)
apply simp
apply(fastsimp simp add:nth_Cons split: nat.split)
done
-lemma listsum_update_nat: "k<size ns \<Longrightarrow>
- listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
+lemma listsum_update_nat:
+ "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
apply(induct ns arbitrary:k)
apply (auto split:nat.split)
apply(drule elem_le_listsum_nat)
@@ -2938,62 +2941,58 @@
"SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
"\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
-lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
+lemma (in monoid_add) listsum_triv:
+ "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
by (induct xs) (simp_all add: left_distrib)
-lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
+lemma (in monoid_add) listsum_0 [simp]:
+ "(\<Sum>x\<leftarrow>xs. 0) = 0"
by (induct xs) (simp_all add: left_distrib)
text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
-lemma uminus_listsum_map:
- fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
- shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
-by (induct xs) simp_all
-
-lemma listsum_addf:
- fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
- shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
-by (induct xs) (simp_all add: algebra_simps)
-
-lemma listsum_subtractf:
- fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
- shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
-by (induct xs) simp_all
-
-lemma listsum_const_mult:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
-by (induct xs, simp_all add: algebra_simps)
-
-lemma listsum_mult_const:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
-by (induct xs, simp_all add: algebra_simps)
-
-lemma listsum_abs:
- fixes xs :: "'a::ordered_ab_group_add_abs list"
- shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
-by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
+lemma (in ab_group_add) uminus_listsum_map:
+ "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
+ by (induct xs) simp_all
+
+lemma (in comm_monoid_add) listsum_addf:
+ "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
+ by (induct xs) (simp_all add: algebra_simps)
+
+lemma (in ab_group_add) listsum_subtractf:
+ "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
+ by (induct xs) (simp_all add: algebra_simps)
+
+lemma (in semiring_0) listsum_const_mult:
+ "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
+ by (induct xs) (simp_all add: algebra_simps)
+
+lemma (in semiring_0) listsum_mult_const:
+ "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
+ by (induct xs) (simp_all add: algebra_simps)
+
+lemma (in ordered_ab_group_add_abs) listsum_abs:
+ "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
+ by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
lemma listsum_mono:
- fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
+ fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
-by (induct xs, simp, simp add: add_mono)
-
-lemma listsum_distinct_conv_setsum_set:
+ by (induct xs) (simp, simp add: add_mono)
+
+lemma (in monoid_add) listsum_distinct_conv_setsum_set:
"distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
by (induct xs) simp_all
-lemma interv_listsum_conv_setsum_set_nat:
+lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
"listsum (map f [m..<n]) = setsum f (set [m..<n])"
by (simp add: listsum_distinct_conv_setsum_set)
-lemma interv_listsum_conv_setsum_set_int:
+lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
"listsum (map f [k..l]) = setsum f (set [k..l])"
by (simp add: listsum_distinct_conv_setsum_set)
text {* General equivalence between @{const listsum} and @{const setsum} *}
-lemma listsum_setsum_nth:
+lemma (in monoid_add) listsum_setsum_nth:
"listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Sep 29 17:59:20 2010 +0200
@@ -18,11 +18,11 @@
section {* Executability of @{term check_bounded} *}
-consts
- list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
-primrec
+
+primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
+where
"list_all'_rec P n [] = True"
- "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
+| "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
definition list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
"list_all' P xs \<equiv> list_all'_rec P 0 xs"
--- a/src/HOL/MicroJava/Comp/TranslComp.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/Comp/TranslComp.thy Wed Sep 29 17:59:20 2010 +0200
@@ -8,71 +8,69 @@
(* parameter java_mb only serves to define function index later *)
-consts
- compExpr :: "java_mb => expr => instr list"
- compExprs :: "java_mb => expr list => instr list"
- compStmt :: "java_mb => stmt => instr list"
-
(**********************************************************************)
(** code generation for expressions **)
-primrec
+primrec compExpr :: "java_mb => expr => instr list"
+ and compExprs :: "java_mb => expr list => instr list"
+where
+
(*class instance creation*)
-"compExpr jmb (NewC c) = [New c]"
+"compExpr jmb (NewC c) = [New c]" |
(*type cast*)
-"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]"
+"compExpr jmb (Cast c e) = compExpr jmb e @ [Checkcast c]" |
(*literals*)
-"compExpr jmb (Lit val) = [LitPush val]"
+"compExpr jmb (Lit val) = [LitPush val]" |
(* binary operation *)
"compExpr jmb (BinOp bo e1 e2) = compExpr jmb e1 @ compExpr jmb e2 @
(case bo of Eq => [Ifcmpeq 3,LitPush(Bool False),Goto 2,LitPush(Bool True)]
- | Add => [IAdd])"
+ | Add => [IAdd])" |
(*local variable*)
-"compExpr jmb (LAcc vn) = [Load (index jmb vn)]"
+"compExpr jmb (LAcc vn) = [Load (index jmb vn)]" |
(*assignement*)
-"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]"
+"compExpr jmb (vn::=e) = compExpr jmb e @ [Dup , Store (index jmb vn)]" |
(*field access*)
-"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]"
+"compExpr jmb ( {cn}e..fn ) = compExpr jmb e @ [Getfield fn cn]" |
(*field assignement - expected syntax: {_}_.._:=_ *)
"compExpr jmb (FAss cn e1 fn e2 ) =
- compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]"
+ compExpr jmb e1 @ compExpr jmb e2 @ [Dup_x1 , Putfield fn cn]" |
(*method call*)
"compExpr jmb (Call cn e1 mn X ps) =
- compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]"
+ compExpr jmb e1 @ compExprs jmb ps @ [Invoke cn mn X]" |
(** code generation expression lists **)
-"compExprs jmb [] = []"
+"compExprs jmb [] = []" |
"compExprs jmb (e#es) = compExpr jmb e @ compExprs jmb es"
-
-primrec
+primrec compStmt :: "java_mb => stmt => instr list" where
+
(** code generation for statements **)
-"compStmt jmb Skip = []"
+"compStmt jmb Skip = []" |
-"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])"
+"compStmt jmb (Expr e) = ((compExpr jmb e) @ [Pop])" |
-"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))"
+"compStmt jmb (c1;; c2) = ((compStmt jmb c1) @ (compStmt jmb c2))" |
"compStmt jmb (If(e) c1 Else c2) =
(let cnstf = LitPush (Bool False);
@@ -82,7 +80,7 @@
test = Ifcmpeq (int(length thn +2));
thnex = Goto (int(length els +1))
in
- [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)"
+ [cnstf] @ cnd @ [test] @ thn @ [thnex] @ els)" |
"compStmt jmb (While(e) c) =
(let cnstf = LitPush (Bool False);
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Wed Sep 29 17:59:20 2010 +0200
@@ -45,16 +45,6 @@
sttp_of :: "method_type \<times> state_type \<Rightarrow> state_type"
where "sttp_of == snd"
-consts
- compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr
- \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
- compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list
- \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
- compTpStmt :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt
- \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
definition nochangeST :: "state_type \<Rightarrow> method_type \<times> state_type" where
"nochangeST sttp == ([Some sttp], sttp)"
@@ -80,60 +70,45 @@
(* Expressions *)
-primrec
-
+primrec compTpExpr :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr \<Rightarrow>
+ state_type \<Rightarrow> method_type \<times> state_type"
+ and compTpExprs :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> expr list \<Rightarrow>
+ state_type \<Rightarrow> method_type \<times> state_type"
+where
"compTpExpr jmb G (NewC c) = pushST [Class c]"
-
- "compTpExpr jmb G (Cast c e) =
- (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
-
- "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
-
- "compTpExpr jmb G (BinOp bo e1 e2) =
+| "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) \<box> (replST 1 (Class c))"
+| "compTpExpr jmb G (Lit val) = pushST [the (typeof (\<lambda>v. None) val)]"
+| "compTpExpr jmb G (BinOp bo e1 e2) =
(compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box>
(case bo of
Eq => popST 2 \<box> pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]
| Add => replST 2 (PrimT Integer))"
-
- "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT).
+| "compTpExpr jmb G (LAcc vn) = (\<lambda> (ST, LT).
pushST [ok_val (LT ! (index jmb vn))] (ST, LT))"
-
- "compTpExpr jmb G (vn::=e) =
+| "compTpExpr jmb G (vn::=e) =
(compTpExpr jmb G e) \<box> dupST \<box> (popST 1)"
-
-
- "compTpExpr jmb G ( {cn}e..fn ) =
+| "compTpExpr jmb G ( {cn}e..fn ) =
(compTpExpr jmb G e) \<box> replST 1 (snd (the (field (G,cn) fn)))"
-
- "compTpExpr jmb G (FAss cn e1 fn e2 ) =
+| "compTpExpr jmb G (FAss cn e1 fn e2 ) =
(compTpExpr jmb G e1) \<box> (compTpExpr jmb G e2) \<box> dup_x1ST \<box> (popST 2)"
-
-
- "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
+| "compTpExpr jmb G ({C}a..mn({fpTs}ps)) =
(compTpExpr jmb G a) \<box> (compTpExprs jmb G ps) \<box>
(replST ((length ps) + 1) (method_rT (the (method (G,C) (mn,fpTs)))))"
-
-
-(* Expression lists *)
-
- "compTpExprs jmb G [] = comb_nil"
-
- "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
+| "compTpExprs jmb G [] = comb_nil"
+| "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \<box> (compTpExprs jmb G es)"
(* Statements *)
-primrec
- "compTpStmt jmb G Skip = comb_nil"
-
- "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) \<box> popST 1"
-
- "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
-
- "compTpStmt jmb G (If(e) c1 Else c2) =
+primrec compTpStmt :: "java_mb \<Rightarrow> java_mb prog \<Rightarrow> stmt \<Rightarrow>
+ state_type \<Rightarrow> method_type \<times> state_type"
+where
+ "compTpStmt jmb G Skip = comb_nil"
+| "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) \<box> popST 1"
+| "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \<box> (compTpStmt jmb G c2)"
+| "compTpStmt jmb G (If(e) c1 Else c2) =
(pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
(compTpStmt jmb G c1) \<box> nochangeST \<box> (compTpStmt jmb G c2)"
-
- "compTpStmt jmb G (While(e) c) =
+| "compTpStmt jmb G (While(e) c) =
(pushST [PrimT Boolean]) \<box> (compTpExpr jmb G e) \<box> popST 2 \<box>
(compTpStmt jmb G c) \<box> nochangeST"
@@ -141,13 +116,11 @@
\<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type" where
"compTpInit jmb == (\<lambda> (vn,ty). (pushST [ty]) \<box> (storeST (index jmb vn) ty))"
-consts
- compTpInitLvars :: "[java_mb, (vname \<times> ty) list]
- \<Rightarrow> state_type \<Rightarrow> method_type \<times> state_type"
-
-primrec
+primrec compTpInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow>
+ state_type \<Rightarrow> method_type \<times> state_type"
+where
"compTpInitLvars jmb [] = comb_nil"
- "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
+| "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \<box> (compTpInitLvars jmb lvars)"
definition start_ST :: "opstack_type" where
"start_ST == []"
--- a/src/HOL/MicroJava/DFA/Err.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy Wed Sep 29 17:59:20 2010 +0200
@@ -47,11 +47,9 @@
where "err_semilat L == semilat(Err.sl L)"
-consts
- strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
-primrec
+primrec strict :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)" where
"strict f Err = Err"
- "strict f (OK x) = f x"
+| "strict f (OK x) = f x"
lemma strict_Some [simp]:
"(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
--- a/src/HOL/MicroJava/J/Value.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Wed Sep 29 17:59:20 2010 +0200
@@ -22,31 +22,22 @@
of clash with HOL/Set.thy"
| Addr loc -- "addresses, i.e. locations of objects "
-consts
- the_Bool :: "val => bool"
- the_Intg :: "val => int"
- the_Addr :: "val => loc"
-
-primrec
+primrec the_Bool :: "val => bool" where
"the_Bool (Bool b) = b"
-primrec
+primrec the_Intg :: "val => int" where
"the_Intg (Intg i) = i"
-primrec
+primrec the_Addr :: "val => loc" where
"the_Addr (Addr a) = a"
-consts
- defpval :: "prim_ty => val" -- "default value for primitive types"
- default_val :: "ty => val" -- "default value for all types"
-
-primrec
+primrec defpval :: "prim_ty => val" -- "default value for primitive types" where
"defpval Void = Unit"
- "defpval Boolean = Bool False"
- "defpval Integer = Intg 0"
+| "defpval Boolean = Bool False"
+| "defpval Integer = Intg 0"
-primrec
+primrec default_val :: "ty => val" -- "default value for all types" where
"default_val (PrimT pt) = defpval pt"
- "default_val (RefT r ) = Null"
+| "default_val (RefT r ) = Null"
end
--- a/src/HOL/MicroJava/J/WellType.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Wed Sep 29 17:59:20 2010 +0200
@@ -73,15 +73,13 @@
THEN max_spec2appl_meths, THEN appl_methsD]
-consts
- typeof :: "(loc => ty option) => val => ty option"
-
-primrec
+primrec typeof :: "(loc => ty option) => val => ty option"
+where
"typeof dt Unit = Some (PrimT Void)"
- "typeof dt Null = Some NT"
- "typeof dt (Bool b) = Some (PrimT Boolean)"
- "typeof dt (Intg i) = Some (PrimT Integer)"
- "typeof dt (Addr a) = dt a"
+| "typeof dt Null = Some NT"
+| "typeof dt (Bool b) = Some (PrimT Boolean)"
+| "typeof dt (Intg i) = Some (PrimT Integer)"
+| "typeof dt (Addr a) = dt a"
lemma is_type_typeof [rule_format (no_asm), simp]:
"(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Wed Sep 29 17:59:20 2010 +0200
@@ -13,12 +13,11 @@
start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
-consts
- match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
- \<Rightarrow> p_count option"
-primrec
+primrec match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
+ \<Rightarrow> p_count option"
+where
"match_exception_table G cn pc [] = None"
- "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
+| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
then Some (fst (snd (snd e)))
else match_exception_table G cn pc es)"
@@ -27,11 +26,11 @@
where "ex_table_of m == snd (snd (snd m))"
-consts
- find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list \<Rightarrow> jvm_state"
-primrec
+primrec find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list
+ \<Rightarrow> jvm_state"
+where
"find_handler G xcpt hp [] = (xcpt, hp, [])"
- "find_handler G xcpt hp (fr#frs) =
+| "find_handler G xcpt hp (fr#frs) =
(case xcpt of
None \<Rightarrow> (None, hp, fr#frs)
| Some xc \<Rightarrow>
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Sep 29 17:59:20 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/JVM/JVMExecInstr.thy
- ID: $Id$
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -11,18 +10,16 @@
theory JVMExecInstr imports JVMInstructions JVMState begin
-consts
- exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars,
- cname, sig, p_count, frame list] => jvm_state"
-primrec
+primrec exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
+where
"exec_instr (Load idx) G hp stk vars Cl sig pc frs =
- (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
+ (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
"exec_instr (Store idx) G hp stk vars Cl sig pc frs =
- (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)"
+ (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)" |
"exec_instr (LitPush v) G hp stk vars Cl sig pc frs =
- (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
+ (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" |
"exec_instr (New C) G hp stk vars Cl sig pc frs =
(let (oref,xp') = new_Addr hp;
@@ -30,7 +27,7 @@
hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
pc' = if xp'=None then pc+1 else pc
in
- (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))"
+ (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))" |
"exec_instr (Getfield F C) G hp stk vars Cl sig pc frs =
(let oref = hd stk;
@@ -38,7 +35,7 @@
(oc,fs) = the(hp(the_Addr oref));
pc' = if xp'=None then pc+1 else pc
in
- (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))"
+ (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))" |
"exec_instr (Putfield F C) G hp stk vars Cl sig pc frs =
(let (fval,oref)= (hd stk, hd(tl stk));
@@ -48,7 +45,7 @@
hp' = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp;
pc' = if xp'=None then pc+1 else pc
in
- (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))"
+ (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))" |
"exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
(let oref = hd stk;
@@ -56,7 +53,7 @@
stk' = if xp'=None then stk else tl stk;
pc' = if xp'=None then pc+1 else pc
in
- (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
+ (xp', hp, (stk', vars, Cl, sig, pc')#frs))" |
"exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
(let n = length ps;
@@ -69,7 +66,7 @@
[([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
else []
in
- (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))"
+ (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" |
-- "Because exception handling needs the pc of the Invoke instruction,"
-- "Invoke doesn't change stk and pc yet (@{text Return} does that)."
@@ -82,42 +79,42 @@
in
(None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))"
-- "Return drops arguments from the caller's stack and increases"
- -- "the program counter in the caller"
+ -- "the program counter in the caller" |
"exec_instr Pop G hp stk vars Cl sig pc frs =
- (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)"
+ (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" |
"exec_instr Dup G hp stk vars Cl sig pc frs =
- (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
+ (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)" |
"exec_instr Dup_x1 G hp stk vars Cl sig pc frs =
(None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)),
- vars, Cl, sig, pc+1)#frs)"
+ vars, Cl, sig, pc+1)#frs)" |
"exec_instr Dup_x2 G hp stk vars Cl sig pc frs =
(None, hp,
(hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
- vars, Cl, sig, pc+1)#frs)"
+ vars, Cl, sig, pc+1)#frs)" |
"exec_instr Swap G hp stk vars Cl sig pc frs =
(let (val1,val2) = (hd stk,hd (tl stk))
in
- (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+ (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))" |
"exec_instr IAdd G hp stk vars Cl sig pc frs =
(let (val1,val2) = (hd stk,hd (tl stk))
in
(None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)),
- vars, Cl, sig, pc+1)#frs))"
+ vars, Cl, sig, pc+1)#frs))" |
"exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
(let (val1,val2) = (hd stk, hd (tl stk));
pc' = if val1 = val2 then nat(int pc+i) else pc+1
in
- (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
+ (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))" |
"exec_instr (Goto i) G hp stk vars Cl sig pc frs =
- (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)"
+ (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)" |
"exec_instr Throw G hp stk vars Cl sig pc frs =
(let xcpt = raise_system_xcpt (hd stk = Null) NullPointer;
--- a/src/HOL/NanoJava/Example.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/NanoJava/Example.thy Wed Sep 29 17:59:20 2010 +0200
@@ -5,7 +5,9 @@
header "Example"
-theory Example imports Equivalence begin
+theory Example
+imports Equivalence
+begin
text {*
@@ -89,9 +91,9 @@
subsection "``atleast'' relation for interpretation of Nat ``values''"
-consts Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50)
-primrec "s:x\<ge>0 = (x\<noteq>Null)"
- "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
+primrec Nat_atleast :: "state \<Rightarrow> val \<Rightarrow> nat \<Rightarrow> bool" ("_:_ \<ge> _" [51, 51, 51] 50) where
+ "s:x\<ge>0 = (x\<noteq>Null)"
+| "s:x\<ge>Suc n = (\<exists>a. x=Addr a \<and> heap s a \<noteq> None \<and> s:get_field s a pred\<ge>n)"
lemma Nat_atleast_lupd [rule_format, simp]:
"\<forall>s v::val. lupd(x\<mapsto>y) s:v \<ge> n = (s:v \<ge> n)"
--- a/src/HOL/Nominal/Examples/Standardization.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy Wed Sep 29 17:59:20 2010 +0200
@@ -213,7 +213,7 @@
prefer 2
apply (erule allE, erule impE, rule refl, erule spec)
apply simp
- apply (metis add_strict_increasing le_add1 length_pos_if_in_set listsum listsum_map_remove1 nat_add_commute)
+ apply (metis add_strict_increasing le_add1 length_pos_if_in_set listsum_foldl listsum_map_remove1 nat_add_commute)
apply clarify
apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
prefer 2
--- a/src/HOL/Nominal/Nominal.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Nominal/Nominal.thy Wed Sep 29 17:59:20 2010 +0200
@@ -10,6 +10,7 @@
("nominal_primrec.ML")
("nominal_inductive.ML")
("nominal_inductive2.ML")
+ ("old_primrec.ML")
begin
section {* Permutations *}
@@ -3604,6 +3605,7 @@
(***************************************)
(* setup for the individial atom-kinds *)
(* and nominal datatypes *)
+use "old_primrec.ML"
use "nominal_atoms.ML"
(************************************************************)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/old_primrec.ML Wed Sep 29 17:59:20 2010 +0200
@@ -0,0 +1,326 @@
+(* Title: HOL/Tools/old_primrec.ML
+ Author: Norbert Voelker, FernUni Hagen
+ Author: Stefan Berghofer, TU Muenchen
+
+Package for defining functions on datatypes by primitive recursion.
+*)
+
+signature OLD_PRIMREC =
+sig
+ val unify_consts: theory -> term list -> term list -> term list * term list
+ val add_primrec: string -> ((bstring * string) * Attrib.src list) list
+ -> theory -> thm list * theory
+ val add_primrec_unchecked: string -> ((bstring * string) * Attrib.src list) list
+ -> theory -> thm list * theory
+ val add_primrec_i: string -> ((bstring * term) * attribute list) list
+ -> theory -> thm list * theory
+ val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
+ -> theory -> thm list * theory
+end;
+
+structure OldPrimrec : OLD_PRIMREC =
+struct
+
+open Datatype_Aux;
+
+exception RecError of string;
+
+fun primrec_err s = error ("Primrec definition error:\n" ^ s);
+fun primrec_eq_err thy s eq =
+ primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
+
+
+(*the following code ensures that each recursive set always has the
+ same type in all introduction rules*)
+fun unify_consts thy cs intr_ts =
+ (let
+ fun varify t (i, ts) =
+ let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify_global [] t))
+ in (maxidx_of_term t', t'::ts) end;
+ val (i, cs') = fold_rev varify cs (~1, []);
+ val (i', intr_ts') = fold_rev varify intr_ts (i, []);
+ val rec_consts = fold Term.add_consts cs' [];
+ val intr_consts = fold Term.add_consts intr_ts' [];
+ fun unify (cname, cT) =
+ let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
+ in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
+ val (env, _) = fold unify rec_consts (Vartab.empty, i');
+ val subst = Type.legacy_freeze o map_types (Envir.norm_type env)
+
+ in (map subst cs', map subst intr_ts')
+ end) handle Type.TUNIFY =>
+ (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
+
+
+(* preprocessing of equations *)
+
+fun process_eqn thy eq rec_fns =
+ let
+ val (lhs, rhs) =
+ if null (Term.add_vars eq []) then
+ HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+ handle TERM _ => raise RecError "not a proper equation"
+ else raise RecError "illegal schematic variable(s)";
+
+ val (recfun, args) = strip_comb lhs;
+ val fnameT = dest_Const recfun handle TERM _ =>
+ raise RecError "function is not declared as constant in theory";
+
+ val (ls', rest) = take_prefix is_Free args;
+ val (middle, rs') = take_suffix is_Free rest;
+ val rpos = length ls';
+
+ val (constr, cargs') = if null middle then raise RecError "constructor missing"
+ else strip_comb (hd middle);
+ val (cname, T) = dest_Const constr
+ handle TERM _ => raise RecError "ill-formed constructor";
+ val (tname, _) = dest_Type (body_type T) handle TYPE _ =>
+ raise RecError "cannot determine datatype associated with function"
+
+ val (ls, cargs, rs) =
+ (map dest_Free ls', map dest_Free cargs', map dest_Free rs')
+ handle TERM _ => raise RecError "illegal argument in pattern";
+ val lfrees = ls @ rs @ cargs;
+
+ fun check_vars _ [] = ()
+ | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
+ in
+ if length middle > 1 then
+ raise RecError "more than one non-variable in pattern"
+ else
+ (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
+ check_vars "extra variables on rhs: "
+ (subtract (op =) lfrees (map dest_Free (OldTerm.term_frees rhs)));
+ case AList.lookup (op =) rec_fns fnameT of
+ NONE =>
+ (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
+ | SOME (_, rpos', eqns) =>
+ if AList.defined (op =) eqns cname then
+ raise RecError "constructor already occurred as pattern"
+ else if rpos <> rpos' then
+ raise RecError "position of recursive argument inconsistent"
+ else
+ AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
+ rec_fns)
+ end
+ handle RecError s => primrec_eq_err thy s eq;
+
+fun process_fun thy descr rec_eqns (i, fnameT as (fname, _)) (fnameTs, fnss) =
+ let
+ val (_, (tname, _, constrs)) = List.nth (descr, i);
+
+ (* substitute "fname ls x rs" by "y ls rs" for (x, (_, y)) in subs *)
+
+ fun subst [] t fs = (t, fs)
+ | subst subs (Abs (a, T, t)) fs =
+ fs
+ |> subst subs t
+ |-> (fn t' => pair (Abs (a, T, t')))
+ | subst subs (t as (_ $ _)) fs =
+ let
+ val (f, ts) = strip_comb t;
+ in
+ if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then
+ let
+ val fnameT' as (fname', _) = dest_Const f;
+ val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
+ val ls = take rpos ts;
+ val rest = drop rpos ts;
+ val (x', rs) = (hd rest, tl rest)
+ handle Empty => raise RecError ("not enough arguments\
+ \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
+ val (x, xs) = strip_comb x'
+ in case AList.lookup (op =) subs x
+ of NONE =>
+ fs
+ |> fold_map (subst subs) ts
+ |-> (fn ts' => pair (list_comb (f, ts')))
+ | SOME (i', y) =>
+ fs
+ |> fold_map (subst subs) (xs @ ls @ rs)
+ ||> process_fun thy descr rec_eqns (i', fnameT')
+ |-> (fn ts' => pair (list_comb (y, ts')))
+ end
+ else
+ fs
+ |> fold_map (subst subs) (f :: ts)
+ |-> (fn (f'::ts') => pair (list_comb (f', ts')))
+ end
+ | subst _ t fs = (t, fs);
+
+ (* translate rec equations into function arguments suitable for rec comb *)
+
+ fun trans eqns (cname, cargs) (fnameTs', fnss', fns) =
+ (case AList.lookup (op =) eqns cname of
+ NONE => (warning ("No equation for constructor " ^ quote cname ^
+ "\nin definition of function " ^ quote fname);
+ (fnameTs', fnss', (Const ("HOL.undefined", dummyT))::fns))
+ | SOME (ls, cargs', rs, rhs, eq) =>
+ let
+ val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
+ val rargs = map fst recs;
+ val subs = map (rpair dummyT o fst)
+ (rev (Term.rename_wrt_term rhs rargs));
+ val (rhs', (fnameTs'', fnss'')) =
+ (subst (map (fn ((x, y), z) =>
+ (Free x, (body_index y, Free z)))
+ (recs ~~ subs)) rhs (fnameTs', fnss'))
+ handle RecError s => primrec_eq_err thy s eq
+ in (fnameTs'', fnss'',
+ (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
+ end)
+
+ in (case AList.lookup (op =) fnameTs i of
+ NONE =>
+ if exists (equal fnameT o snd) fnameTs then
+ raise RecError ("inconsistent functions for datatype " ^ quote tname)
+ else
+ let
+ val (_, _, eqns) = the (AList.lookup (op =) rec_eqns fnameT);
+ val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs
+ ((i, fnameT)::fnameTs, fnss, [])
+ in
+ (fnameTs', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
+ end
+ | SOME fnameT' =>
+ if fnameT = fnameT' then (fnameTs, fnss)
+ else raise RecError ("inconsistent functions for datatype " ^ quote tname))
+ end;
+
+
+(* prepare functions needed for definitions *)
+
+fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
+ case AList.lookup (op =) fns i of
+ NONE =>
+ let
+ val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
+ replicate (length cargs + length (filter is_rec_type cargs))
+ dummyT ---> HOLogic.unitT)) constrs;
+ val _ = warning ("No function definition for datatype " ^ quote tname)
+ in
+ (dummy_fns @ fs, defs)
+ end
+ | SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name, tname) :: defs);
+
+
+(* make definition *)
+
+fun make_def thy fs (fname, ls, rec_name, tname) =
+ let
+ val rhs = fold_rev (fn T => fn t => Abs ("", T, t))
+ ((map snd ls) @ [dummyT])
+ (list_comb (Const (rec_name, dummyT),
+ fs @ map Bound (0 ::(length ls downto 1))))
+ val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
+ val def_prop =
+ singleton (Syntax.check_terms (ProofContext.init_global thy))
+ (Logic.mk_equals (Const (fname, dummyT), rhs));
+ in (def_name, def_prop) end;
+
+
+(* find datatypes which contain all datatypes in tnames' *)
+
+fun find_dts (dt_info : info Symtab.table) _ [] = []
+ | find_dts dt_info tnames' (tname::tnames) =
+ (case Symtab.lookup dt_info tname of
+ NONE => primrec_err (quote tname ^ " is not a datatype")
+ | SOME dt =>
+ if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
+ (tname, dt)::(find_dts dt_info tnames' tnames)
+ else find_dts dt_info tnames' tnames);
+
+fun prepare_induct ({descr, induct, ...}: info) rec_eqns =
+ let
+ fun constrs_of (_, (_, _, cs)) =
+ map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
+ val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
+ in
+ induct
+ |> Rule_Cases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
+ |> Rule_Cases.save induct
+ end;
+
+local
+
+fun gen_primrec_i note def alt_name eqns_atts thy =
+ let
+ val (eqns, atts) = split_list eqns_atts;
+ val dt_info = Datatype_Data.get_all thy;
+ val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ;
+ val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
+ val dts = find_dts dt_info tnames tnames;
+ val main_fns =
+ map (fn (tname, {index, ...}) =>
+ (index,
+ (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
+ dts;
+ val {descr, rec_names, rec_rewrites, ...} =
+ if null dts then
+ primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
+ else snd (hd dts);
+ val (fnameTs, fnss) =
+ fold_rev (process_fun thy descr rec_eqns) main_fns ([], []);
+ val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
+ val defs' = map (make_def thy fs) defs;
+ val nameTs1 = map snd fnameTs;
+ val nameTs2 = map fst rec_eqns;
+ val _ = if eq_set (op =) (nameTs1, nameTs2) then ()
+ else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
+ "\nare not mutually recursive");
+ val primrec_name =
+ if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name;
+ val (defs_thms', thy') =
+ thy
+ |> Sign.add_path primrec_name
+ |> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
+ val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';
+ val simps = map (fn (_, t) => Goal.prove_global thy' [] [] t
+ (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
+ val (simps', thy'') =
+ thy'
+ |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
+ val simps'' = maps snd simps';
+ val lhss = map (Logic.varify_global o fst o Logic.dest_equals o snd) defs';
+ in
+ thy''
+ |> note (("simps",
+ [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
+ |> snd
+ |> Spec_Rules.add_global Spec_Rules.Equational (lhss, simps)
+ |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
+ |> snd
+ |> Sign.parent_path
+ |> pair simps''
+ end;
+
+fun gen_primrec note def alt_name eqns thy =
+ let
+ val ((names, strings), srcss) = apfst split_list (split_list eqns);
+ val atts = map (map (Attrib.attribute thy)) srcss;
+ val eqn_ts = map (fn s => Syntax.read_prop_global thy s
+ handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
+ val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
+ handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
+ val (_, eqn_ts') = unify_consts thy rec_ts eqn_ts
+ in
+ gen_primrec_i note def alt_name (names ~~ eqn_ts' ~~ atts) thy
+ end;
+
+fun thy_note ((name, atts), thms) =
+ Global_Theory.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
+fun thy_def false ((name, atts), t) =
+ Global_Theory.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
+ | thy_def true ((name, atts), t) =
+ Global_Theory.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
+
+in
+
+val add_primrec = gen_primrec thy_note (thy_def false);
+val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
+val add_primrec_i = gen_primrec_i thy_note (thy_def false);
+val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
+
+end;
+
+end;
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 29 17:59:20 2010 +0200
@@ -1483,6 +1483,60 @@
thm detect_switches9.equation
+text {* The higher-order predicate r is in an output term *}
+
+datatype result = Result bool
+
+inductive fixed_relation :: "'a => bool"
+
+inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
+where
+ "test_relation_in_output_terms r x (Result (r x))"
+| "test_relation_in_output_terms r x (Result (fixed_relation x))"
+
+code_pred test_relation_in_output_terms .
+
+thm test_relation_in_output_terms.equation
+
+
+text {*
+ We want that the argument r is not treated as a higher-order relation, but simply as input.
+*}
+
+inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
+where
+ "list_all r xs ==> test_uninterpreted_relation r xs"
+
+code_pred (modes: i => i => bool) test_uninterpreted_relation .
+
+thm test_uninterpreted_relation.equation
+
+inductive list_ex'
+where
+ "P x ==> list_ex' P (x#xs)"
+| "list_ex' P xs ==> list_ex' P (x#xs)"
+
+code_pred list_ex' .
+
+inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
+where
+ "list_ex r xs ==> test_uninterpreted_relation2 r xs"
+| "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
+
+text {* Proof procedure cannot handle this situation yet. *}
+
+code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
+
+thm test_uninterpreted_relation2.equation
+
+
+text {* Trivial predicate *}
+
+inductive implies_itself :: "'a => bool"
+where
+ "implies_itself x ==> implies_itself x"
+
+code_pred implies_itself .
end
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Sep 29 17:59:20 2010 +0200
@@ -21,44 +21,36 @@
subsection{*Predicate Formalizing the Encryption Association between Keys *}
-consts
- KeyCryptKey :: "[key, key, event list] => bool"
-
-primrec
-
-KeyCryptKey_Nil:
- "KeyCryptKey DK K [] = False"
-
-KeyCryptKey_Cons:
+primrec KeyCryptKey :: "[key, key, event list] => bool"
+where
+ KeyCryptKey_Nil:
+ "KeyCryptKey DK K [] = False"
+| KeyCryptKey_Cons:
--{*Says is the only important case.
1st case: CR5, where KC3 encrypts KC2.
2nd case: any use of priEK C.
Revision 1.12 has a more complicated version with separate treatment of
the dependency of KC1, KC2 and KC3 on priEK (CA i.) Not needed since
priEK C is never sent (and so can't be lost except at the start). *}
- "KeyCryptKey DK K (ev # evs) =
- (KeyCryptKey DK K evs |
- (case ev of
- Says A B Z =>
- ((\<exists>N X Y. A \<noteq> Spy &
+ "KeyCryptKey DK K (ev # evs) =
+ (KeyCryptKey DK K evs |
+ (case ev of
+ Says A B Z =>
+ ((\<exists>N X Y. A \<noteq> Spy &
DK \<in> symKeys &
Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
- (\<exists>C. DK = priEK C))
- | Gets A' X => False
- | Notes A' X => False))"
+ (\<exists>C. DK = priEK C))
+ | Gets A' X => False
+ | Notes A' X => False))"
subsection{*Predicate formalizing the association between keys and nonces *}
-consts
- KeyCryptNonce :: "[key, key, event list] => bool"
-
-primrec
-
-KeyCryptNonce_Nil:
- "KeyCryptNonce EK K [] = False"
-
-KeyCryptNonce_Cons:
+primrec KeyCryptNonce :: "[key, key, event list] => bool"
+where
+ KeyCryptNonce_Nil:
+ "KeyCryptNonce EK K [] = False"
+| KeyCryptNonce_Cons:
--{*Says is the only important case.
1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
2nd case: CR5, where KC3 encrypts NC3;
--- a/src/HOL/SET_Protocol/Event_SET.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/SET_Protocol/Event_SET.thy Wed Sep 29 17:59:20 2010 +0200
@@ -35,15 +35,14 @@
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
- knows :: "[agent, event list] => msg set"
(* Message reception does not extend spy's knowledge because of
reception invariant enforced by Reception rule in protocol definition*)
-primrec
-
-knows_Nil:
- "knows A [] = initState A"
-knows_Cons:
+primrec knows :: "[agent, event list] => msg set"
+where
+ knows_Nil:
+ "knows A [] = initState A"
+| knows_Cons:
"knows A (ev # evs) =
(if A = Spy then
(case ev of
@@ -63,15 +62,13 @@
subsection{*Used Messages*}
-consts
+primrec used :: "event list => msg set"
+where
(*Set of items that might be visible to somebody:
- complement of the set of fresh items*)
- used :: "event list => msg set"
-
-(* As above, message reception does extend used items *)
-primrec
+ complement of the set of fresh items.
+ As above, message reception does extend used items *)
used_Nil: "used [] = (UN B. parts (initState B))"
- used_Cons: "used (ev # evs) =
+| used_Cons: "used (ev # evs) =
(case ev of
Says A B X => parts {X} Un (used evs)
| Gets A X => used evs
--- a/src/HOL/SET_Protocol/Public_SET.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy Wed Sep 29 17:59:20 2010 +0200
@@ -64,7 +64,11 @@
RCA and CAs know their own respective keys;
RCA (has already certified and therefore) knows all CAs public keys;
Spy knows all keys of all bad agents.*}
-primrec
+
+overloading initState \<equiv> "initState"
+begin
+
+primrec initState where
(*<*)
initState_CA:
"initState (CA i) =
@@ -74,29 +78,31 @@
Key (pubEK (CA i)), Key (pubSK (CA i)),
Key (pubEK RCA), Key (pubSK RCA)})"
- initState_Cardholder:
+| initState_Cardholder:
"initState (Cardholder i) =
{Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
Key (pubEK RCA), Key (pubSK RCA)}"
- initState_Merchant:
+| initState_Merchant:
"initState (Merchant i) =
{Key (priEK (Merchant i)), Key (priSK (Merchant i)),
Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
Key (pubEK RCA), Key (pubSK RCA)}"
- initState_PG:
+| initState_PG:
"initState (PG i) =
{Key (priEK (PG i)), Key (priSK (PG i)),
Key (pubEK (PG i)), Key (pubSK (PG i)),
Key (pubEK RCA), Key (pubSK RCA)}"
(*>*)
- initState_Spy:
+| initState_Spy:
"initState Spy = Key ` (invKey ` pubEK ` bad Un
invKey ` pubSK ` bad Un
range pubEK Un range pubSK)"
+end
+
text{*Injective mapping from agents to PANs: an agent can have only one card*}
--- a/src/HOL/SET_Protocol/ROOT.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/SET_Protocol/ROOT.ML Wed Sep 29 17:59:20 2010 +0200
@@ -1,9 +1,3 @@
-(* Title: HOL/SET_Protocol/ROOT.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2003 University of Cambridge
-
-Root file for the SET protocol proofs.
-*)
no_document use_thys ["Nat_Bijection"];
-use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
+use_thys ["SET_Protocol"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET_Protocol/SET_Protocol.thy Wed Sep 29 17:59:20 2010 +0200
@@ -0,0 +1,12 @@
+(* Title: HOL/SET_Protocol/SET_Protocol.thy
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2003 University of Cambridge
+
+Root file for the SET protocol proofs.
+*)
+
+theory SET_Protocol
+imports Cardholder_Registration Merchant_Registration Purchase
+begin
+
+end
--- a/src/HOL/Tools/Datatype/datatype_selectors.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_selectors.ML Wed Sep 29 17:59:20 2010 +0200
@@ -26,7 +26,7 @@
type T = string Stringinttab.table
val empty = Stringinttab.empty
val extend = I
- val merge = Stringinttab.merge (K true)
+ fun merge data : T = Stringinttab.merge (K true) data
)
fun pretty_term context = Syntax.pretty_term (Context.proof_of context)
--- a/src/HOL/Tools/Function/function.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Wed Sep 29 17:59:20 2010 +0200
@@ -52,8 +52,7 @@
Nitpick_Simps.add]
val psimp_attribs = map (Attrib.internal o K)
- [Simplifier.simp_add,
- Nitpick_Psimps.add]
+ [Nitpick_Psimps.add]
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
--- a/src/HOL/Tools/Function/function_lib.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Wed Sep 29 17:59:20 2010 +0200
@@ -18,17 +18,6 @@
fun plural sg pl [x] = sg
| plural sg pl _ = pl
-(* lambda-abstracts over an arbitrarily nested tuple
- ==> hologic.ML? *)
-fun tupled_lambda vars t =
- case vars of
- (Free v) => lambda (Free v) t
- | (Var v) => lambda (Var v) t
- | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
- (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
- | _ => raise Match
-
-
fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
let
val (n, body) = Term.dest_abs a
--- a/src/HOL/Tools/Function/induction_schema.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Wed Sep 29 17:59:20 2010 +0200
@@ -196,7 +196,7 @@
|> fold_rev (Logic.all o Free) ws
|> term_conv thy ind_atomize
|> Object_Logic.drop_judgment thy
- |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
+ |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
in
SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
end
--- a/src/HOL/Tools/Function/mutual.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Wed Sep 29 17:59:20 2010 +0200
@@ -221,7 +221,7 @@
val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
val atup = foldr1 HOLogic.mk_prod avars
in
- tupled_lambda atup (list_comb (P, avars))
+ HOLogic.tupled_lambda atup (list_comb (P, avars))
end
val Ps = map2 mk_P parts newPs
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Sep 29 17:59:20 2010 +0200
@@ -369,7 +369,7 @@
let
val options = Predicate_Compile_Aux.default_options
val mode_analysis_options =
- {use_random = true, reorder_premises = true, infer_pos_and_neg_modes = true}
+ {use_generators = true, reorder_premises = true, infer_pos_and_neg_modes = true}
fun infer prednames (gr, (pos_modes, neg_modes, random)) =
let
val (lookup_modes, lookup_neg_modes, needs_random) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Sep 29 17:59:20 2010 +0200
@@ -145,6 +145,7 @@
(* conversions *)
val imp_prems_conv : conv -> conv
(* simple transformations *)
+ val split_conjuncts_in_assms : Proof.context -> thm -> thm
val expand_tuples : theory -> thm -> thm
val eta_contract_ho_arguments : theory -> thm -> thm
val remove_equalities : theory -> thm -> thm
@@ -821,6 +822,19 @@
val (_, args) = strip_comb atom
in rewrite_args args end
+fun split_conjuncts_in_assms ctxt th =
+ let
+ val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt
+ fun split_conjs i nprems th =
+ if i > nprems then th
+ else
+ case try Drule.RSN (@{thm conjI}, (i, th)) of
+ SOME th' => split_conjs i (nprems+1) th'
+ | NONE => split_conjs (i+1) nprems th
+ in
+ singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
+ end
+
fun expand_tuples thy intro =
let
val ctxt = ProofContext.init_global thy
@@ -840,9 +854,7 @@
(HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
intro'''
(* splitting conjunctions introduced by Pair_eq*)
- fun split_conj prem =
- map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
- val intro''''' = map_term thy (maps_premises split_conj) intro''''
+ val intro''''' = split_conjuncts_in_assms ctxt intro''''
in
intro'''''
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 29 17:59:20 2010 +0200
@@ -68,7 +68,10 @@
val prepare_intrs : options -> Proof.context -> string list -> thm list ->
((string * typ) list * string list * string list * (string * mode list) list *
(string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
- type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
+ type mode_analysis_options =
+ {use_generators : bool,
+ reorder_premises : bool,
+ infer_pos_and_neg_modes : bool}
datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
| Mode_Pair of mode_derivation * mode_derivation | Term of mode
val head_mode_of : mode_derivation -> mode
@@ -431,19 +434,33 @@
fun check_matches_type ctxt predname T ms =
let
fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
- | check m (T as Type("fun", _)) =
- if body_type T = @{typ bool} then false else (m = Input orelse m = Output)
+ | check m (T as Type("fun", _)) = (m = Input orelse m = Output)
| check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
check m1 T1 andalso check m2 T2
| check Input T = true
| check Output T = true
| check Bool @{typ bool} = true
| check _ _ = false
+ fun check_consistent_modes ms =
+ if forall (fn Fun (m1', m2') => true | _ => false) ms then
+ pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
+ |> (fn (res1, res2) => res1 andalso res2)
+ else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
+ true
+ else if forall (fn Bool => true | _ => false) ms then
+ true
+ else
+ false
val _ = map
(fn mode =>
- if (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
+ if length (strip_fun_mode mode) = length (binder_types T)
+ andalso (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
else error (string_of_mode mode ^ " is not a valid mode for " ^ Syntax.string_of_typ ctxt T
^ " at predicate " ^ predname)) ms
+ val _ =
+ if check_consistent_modes ms then ()
+ else error (commas (map string_of_mode ms) ^
+ " are inconsistent modes for predicate " ^ predname)
in
ms
end
@@ -1052,7 +1069,10 @@
(** mode analysis **)
-type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
+type mode_analysis_options =
+ {use_generators : bool,
+ reorder_premises : bool,
+ infer_pos_and_neg_modes : bool}
fun is_constrt thy =
let
@@ -1340,7 +1360,7 @@
(* prefer non-random modes *)
fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
- if random_mode_in_deriv modes t1 deriv1 then 1 else 0)
+ if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
(* prefer modes with more input and less output *)
fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
int_ord (number_of_output_positions (head_mode_of deriv1),
@@ -1411,7 +1431,7 @@
SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
(known_vs_after p vs) (filter_out (equal p) ps)
| SOME (p, SOME (deriv, missing_vars)) =>
- if #use_random mode_analysis_options andalso pol then
+ if #use_generators mode_analysis_options andalso pol then
check_mode_prems ((p, deriv) :: (map
(fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
(distinct (op =) missing_vars))
@@ -1426,7 +1446,7 @@
if forall (is_constructable vs) (in_ts @ out_ts) then
SOME (ts, rev acc_ps, rnd)
else
- if #use_random mode_analysis_options andalso pol then
+ if #use_generators mode_analysis_options andalso pol then
let
val generators = map
(fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
@@ -1676,7 +1696,13 @@
ctxt name mode,
Comp_Mod.funT_of compilation_modifiers mode T)))
| (Free (s, T), Context m) =>
- SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+ (case (AList.lookup (op =) param_modes s) of
+ SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+ | NONE =>
+ let
+ val bs = map (pair "x") (binder_types (fastype_of t))
+ val bounds = map Bound (rev (0 upto (length bs) - 1))
+ in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end)
| (t, Context m) =>
let
val bs = map (pair "x") (binder_types (fastype_of t))
@@ -1711,9 +1737,11 @@
fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
out_ts'' (names', map (rpair []) vs);
+ val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
+ ctxt param_modes) out_ts
in
compile_match constr_vs (eqs @ eqs') out_ts'''
- (mk_single compfuns (HOLogic.mk_tuple out_ts))
+ (mk_single compfuns (HOLogic.mk_tuple processed_out_ts))
end
| compile_prems out_ts vs names ((p, deriv) :: ps) =
let
@@ -1999,12 +2027,6 @@
(fn NONE => "X" | SOME k' => string_of_int k')
(ks @ [SOME k]))) arities));
-fun split_lambda (x as Free _) t = lambda x t
- | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
- HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
- | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
- | split_lambda t _ = raise (TERM ("split_lambda", [t]))
-
fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
@@ -2029,7 +2051,7 @@
val x = Name.variant names "x"
val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
- val t = fold_rev split_lambda args (PredicateCompFuns.mk_Eval
+ val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
(list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
in
(if is_eval then t else Free (x, funT), x :: names)
@@ -2120,8 +2142,8 @@
val (r, _) = PredicateCompFuns.dest_Eval t'
in (SOME (fst (strip_comb r)), NONE) end
val (inargs, outargs) = split_map_mode strip_eval mode args
- val predterm = fold_rev split_lambda inargs
- (PredicateCompFuns.mk_Enum (split_lambda (HOLogic.mk_tuple outargs)
+ val predterm = fold_rev HOLogic.tupled_lambda inargs
+ (PredicateCompFuns.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
(list_comb (Const (name, T), args))))
val lhs = Const (mode_cname, funT)
val def = Logic.mk_equals (lhs, predterm)
@@ -2268,12 +2290,14 @@
if valid_expr expr then
((*tracing "expression is valid";*) Seq.single st)
else
- ((*tracing "expression is not valid";*) Seq.empty) (*error "check_format: wrong format"*)
+ ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
end
-fun prove_match options ctxt out_ts =
+fun prove_match options ctxt nargs out_ts =
let
val thy = ProofContext.theory_of ctxt
+ val eval_if_P =
+ @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp}
fun get_case_rewrite t =
if (is_constructor thy t) then let
val case_rewrites = (#case_rewrites (Datatype.the_info thy
@@ -2287,12 +2311,22 @@
(* make this simpset better! *)
asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
THEN print_tac options "after prove_match:"
- THEN (DETERM (TRY (EqSubst.eqsubst_tac ctxt [0] [@{thm HOL.if_P}] 1
- THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
- THEN print_tac options "if condition to be solved:"
- THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac options "after if simp; in SOLVED:"))
- THEN check_format thy
- THEN print_tac options "after if simplification - a TRY block")))
+ THEN (DETERM (TRY
+ (rtac eval_if_P 1
+ THEN (SUBPROOF (fn {context = ctxt, params, prems, asms, concl, schematics} =>
+ (REPEAT_DETERM (rtac @{thm conjI} 1
+ THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
+ THEN print_tac options "if condition to be solved:"
+ THEN asm_simp_tac HOL_basic_ss' 1
+ THEN TRY (
+ let
+ val prems' = maps dest_conjunct_prem (take nargs prems)
+ in
+ MetaSimplifier.rewrite_goal_tac
+ (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ end
+ THEN REPEAT_DETERM (rtac @{thm refl} 1))
+ THEN print_tac options "after if simp; in SUBPROOF") ctxt 1))))
THEN print_tac options "after if simplification"
end;
@@ -2320,10 +2354,18 @@
let
val (in_ts, clause_out_ts) = split_mode mode ts;
fun prove_prems out_ts [] =
- (prove_match options ctxt out_ts)
+ (prove_match options ctxt nargs out_ts)
THEN print_tac options "before simplifying assumptions"
THEN asm_full_simp_tac HOL_basic_ss' 1
THEN print_tac options "before single intro rule"
+ THEN Subgoal.FOCUS_PREMS
+ (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+ let
+ val prems' = maps dest_conjunct_prem (take nargs prems)
+ in
+ MetaSimplifier.rewrite_goal_tac
+ (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ end) ctxt 1
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
| prove_prems out_ts ((p, deriv) :: ps) =
let
@@ -2362,9 +2404,10 @@
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
THEN (if (is_some name) then
print_tac options "before applying not introduction rule"
- THEN rotate_tac premposition 1
- THEN etac (the neg_intro_rule) 1
- THEN rotate_tac (~premposition) 1
+ THEN Subgoal.FOCUS_PREMS
+ (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+ rtac (the neg_intro_rule) 1
+ THEN rtac (nth prems premposition) 1) ctxt 1
THEN print_tac options "after applying not introduction rule"
THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
THEN (REPEAT_DETERM (atac 1))
@@ -2382,7 +2425,7 @@
THEN prove_sidecond ctxt t
THEN print_tac options "after sidecond:"
THEN prove_prems [] ps)
- in (prove_match options ctxt out_ts)
+ in (prove_match options ctxt nargs out_ts)
THEN rest_tac
end;
val prems_tac = prove_prems in_ts moded_ps
@@ -2519,15 +2562,17 @@
THEN (etac @{thm singleE} 1)
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac HOL_basic_ss' 1)
- THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
- THEN (asm_full_simp_tac HOL_basic_ss' 1)
- THEN SOLVED (print_tac options "state before applying intro rule:"
- THEN (rtac pred_intro_rule
- (* How to handle equality correctly? *)
- THEN_ALL_NEW (K (print_tac options "state before assumption matching")
- THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
- THEN' (K (print_tac options "state after pre-simplification:"))
- THEN' (K (print_tac options "state after assumption matching:")))) 1)
+ THEN TRY (
+ (REPEAT_DETERM (etac @{thm Pair_inject} 1))
+ THEN (asm_full_simp_tac HOL_basic_ss' 1)
+
+ THEN SOLVED (print_tac options "state before applying intro rule:"
+ THEN (rtac pred_intro_rule
+ (* How to handle equality correctly? *)
+ THEN_ALL_NEW (K (print_tac options "state before assumption matching")
+ THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
+ THEN' (K (print_tac options "state after pre-simplification:"))
+ THEN' (K (print_tac options "state after assumption matching:")))) 1))
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
val mode = head_mode_of deriv
@@ -2681,8 +2726,9 @@
[] =>
let
val T = snd (hd preds)
+ val one_mode = hd (the (AList.lookup (op =) all_modes (fst (hd preds))))
val paramTs =
- ho_argsT_of_typ (binder_types T)
+ ho_argsT_of one_mode (binder_types T)
val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
(1 upto length paramTs))
in
@@ -2690,9 +2736,10 @@
end
| (intr :: _) =>
let
- val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+ val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+ val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
in
- ho_args_of_typ (snd (dest_Const p)) args
+ ho_args_of one_mode args
end
val param_vs = map (fst o dest_Free) params
fun add_clause intr clauses =
@@ -2796,7 +2843,7 @@
add_code_equations : Proof.context -> (string * typ) list
-> (string * thm list) list -> (string * thm list) list,
comp_modifiers : Comp_Mod.comp_modifiers,
- use_random : bool,
+ use_generators : bool,
qname : bstring
}
@@ -2907,10 +2954,10 @@
(fn preds => fn thy =>
if not (forall (defined (ProofContext.init_global thy)) preds) then
let
- val mode_analysis_options = {use_random = #use_random (dest_steps steps),
+ val mode_analysis_options = {use_generators = #use_generators (dest_steps steps),
reorder_premises =
not (no_topmost_reordering options andalso not (null (inter (op =) preds names))),
- infer_pos_and_neg_modes = #use_random (dest_steps steps)}
+ infer_pos_and_neg_modes = #use_generators (dest_steps steps)}
in
add_equations_of steps mode_analysis_options options preds thy
end
@@ -2927,7 +2974,7 @@
prove = prove,
add_code_equations = add_code_equations,
comp_modifiers = predicate_comp_modifiers,
- use_random = false,
+ use_generators = false,
qname = "equation"})
val add_depth_limited_equations = gen_add_equations
@@ -2939,7 +2986,7 @@
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = depth_limited_comp_modifiers,
- use_random = false,
+ use_generators = false,
qname = "depth_limited_equation"})
val add_annotated_equations = gen_add_equations
@@ -2951,7 +2998,7 @@
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = annotated_comp_modifiers,
- use_random = false,
+ use_generators = false,
qname = "annotated_equation"})
val add_random_equations = gen_add_equations
@@ -2963,7 +3010,7 @@
comp_modifiers = random_comp_modifiers,
prove = prove_by_skip,
add_code_equations = K (K I),
- use_random = true,
+ use_generators = true,
qname = "random_equation"})
val add_depth_limited_random_equations = gen_add_equations
@@ -2975,7 +3022,7 @@
comp_modifiers = depth_limited_random_comp_modifiers,
prove = prove_by_skip,
add_code_equations = K (K I),
- use_random = true,
+ use_generators = true,
qname = "depth_limited_random_equation"})
val add_dseq_equations = gen_add_equations
@@ -2987,7 +3034,7 @@
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = dseq_comp_modifiers,
- use_random = false,
+ use_generators = false,
qname = "dseq_equation"})
val add_random_dseq_equations = gen_add_equations
@@ -3005,7 +3052,7 @@
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = pos_random_dseq_comp_modifiers,
- use_random = true,
+ use_generators = true,
qname = "random_dseq_equation"})
val add_new_random_dseq_equations = gen_add_equations
@@ -3023,7 +3070,7 @@
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = new_pos_random_dseq_comp_modifiers,
- use_random = true,
+ use_generators = true,
qname = "new_random_dseq_equation"})
(** user interface **)
@@ -3224,7 +3271,7 @@
val t_pred = compile_expr comp_modifiers ctxt
(body, deriv) [] additional_arguments;
val T_pred = dest_predT compfuns (fastype_of t_pred)
- val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
+ val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output_tuple
in
if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Sep 29 17:59:20 2010 +0200
@@ -178,17 +178,6 @@
|> maps (fn (res, (names, prems)) =>
flatten' (betapply (g, res)) (names, prems))
end)
- | Const (@{const_name prod_case}, _) =>
- (let
- val (_, g :: res :: args) = strip_comb t
- val [res1, res2] = Name.variant_list names ["res1", "res2"]
- val (T1, T2) = HOLogic.dest_prodT (fastype_of res)
- val (resv1, resv2) = (Free (res1, T1), Free (res2, T2))
- in
- flatten' (betapplys (g, (resv1 :: resv2 :: args)))
- (res1 :: res2 :: names,
- HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
- end)
| _ =>
case find_split_thm thy (fst (strip_comb t)) of
SOME raw_split_thm =>
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Sep 29 17:59:20 2010 +0200
@@ -256,34 +256,18 @@
#> Conv.fconv_rule nnf_conv
#> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
-fun split_conjs thy t =
- let
- fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
- (split_conjunctions t1) @ (split_conjunctions t2)
- | split_conjunctions t = [t]
- in
- map HOLogic.mk_Trueprop (split_conjunctions (HOLogic.dest_Trueprop t))
- end
-
fun rewrite_intros thy =
Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
#> Simplifier.full_simplify
(HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
- #> map_term thy (maps_premises (split_conjs thy))
+ #> split_conjuncts_in_assms (ProofContext.init_global thy)
fun print_specs options thy msg ths =
if show_intermediate_results options then
(tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
else
()
-(*
-fun split_cases thy th =
- let
-
- in
- map_term thy th
- end
-*)
+
fun preprocess options (constname, specs) thy =
(* case Predicate_Compile_Data.processed_specs thy constname of
SOME specss => (specss, thy)
@@ -292,7 +276,7 @@
val ctxt = ProofContext.init_global thy
val intros =
if forall is_pred_equation specs then
- map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
+ map (split_conjuncts_in_assms ctxt) (introrulify thy (map rewrite specs))
else if forall (is_intro constname) specs then
map (rewrite_intros thy) specs
else
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 29 17:59:20 2010 +0200
@@ -177,15 +177,7 @@
val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
-fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
- | mk_split_lambda [x] t = lambda x t
- | mk_split_lambda xs t =
- let
- fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
- | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
- in
- mk_split_lambda' xs t
- end;
+val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
fun cpu_time description f =
let
--- a/src/HOL/Tools/hologic.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Wed Sep 29 17:59:20 2010 +0200
@@ -67,6 +67,7 @@
val split_const: typ * typ * typ -> term
val mk_split: term -> term
val flatten_tupleT: typ -> typ list
+ val tupled_lambda: term -> term -> term
val mk_tupleT: typ list -> typ
val strip_tupleT: typ -> typ list
val mk_tuple: term list -> term
@@ -327,6 +328,15 @@
fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
| flatten_tupleT T = [T];
+(*abstraction over nested tuples*)
+fun tupled_lambda (x as Free _) b = lambda x b
+ | tupled_lambda (x as Var _) b = lambda x b
+ | tupled_lambda (Const ("Product_Type.Pair", _) $ u $ v) b =
+ mk_split (tupled_lambda u (tupled_lambda v b))
+ | tupled_lambda (Const ("Product_Type.Unity", _)) b =
+ Abs ("x", unitT, b)
+ | tupled_lambda t _ = raise TERM ("tupled_lambda: bad tuple", [t]);
+
(* tuples with right-fold structure *)
--- a/src/HOL/Tools/old_primrec.ML Wed Sep 29 17:58:27 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,326 +0,0 @@
-(* Title: HOL/Tools/old_primrec.ML
- Author: Norbert Voelker, FernUni Hagen
- Author: Stefan Berghofer, TU Muenchen
-
-Package for defining functions on datatypes by primitive recursion.
-*)
-
-signature OLD_PRIMREC =
-sig
- val unify_consts: theory -> term list -> term list -> term list * term list
- val add_primrec: string -> ((bstring * string) * Attrib.src list) list
- -> theory -> thm list * theory
- val add_primrec_unchecked: string -> ((bstring * string) * Attrib.src list) list
- -> theory -> thm list * theory
- val add_primrec_i: string -> ((bstring * term) * attribute list) list
- -> theory -> thm list * theory
- val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
- -> theory -> thm list * theory
-end;
-
-structure OldPrimrec : OLD_PRIMREC =
-struct
-
-open Datatype_Aux;
-
-exception RecError of string;
-
-fun primrec_err s = error ("Primrec definition error:\n" ^ s);
-fun primrec_eq_err thy s eq =
- primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
-
-
-(*the following code ensures that each recursive set always has the
- same type in all introduction rules*)
-fun unify_consts thy cs intr_ts =
- (let
- fun varify t (i, ts) =
- let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify_global [] t))
- in (maxidx_of_term t', t'::ts) end;
- val (i, cs') = fold_rev varify cs (~1, []);
- val (i', intr_ts') = fold_rev varify intr_ts (i, []);
- val rec_consts = fold Term.add_consts cs' [];
- val intr_consts = fold Term.add_consts intr_ts' [];
- fun unify (cname, cT) =
- let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
- in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
- val (env, _) = fold unify rec_consts (Vartab.empty, i');
- val subst = Type.legacy_freeze o map_types (Envir.norm_type env)
-
- in (map subst cs', map subst intr_ts')
- end) handle Type.TUNIFY =>
- (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
-
-
-(* preprocessing of equations *)
-
-fun process_eqn thy eq rec_fns =
- let
- val (lhs, rhs) =
- if null (Term.add_vars eq []) then
- HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
- handle TERM _ => raise RecError "not a proper equation"
- else raise RecError "illegal schematic variable(s)";
-
- val (recfun, args) = strip_comb lhs;
- val fnameT = dest_Const recfun handle TERM _ =>
- raise RecError "function is not declared as constant in theory";
-
- val (ls', rest) = take_prefix is_Free args;
- val (middle, rs') = take_suffix is_Free rest;
- val rpos = length ls';
-
- val (constr, cargs') = if null middle then raise RecError "constructor missing"
- else strip_comb (hd middle);
- val (cname, T) = dest_Const constr
- handle TERM _ => raise RecError "ill-formed constructor";
- val (tname, _) = dest_Type (body_type T) handle TYPE _ =>
- raise RecError "cannot determine datatype associated with function"
-
- val (ls, cargs, rs) =
- (map dest_Free ls', map dest_Free cargs', map dest_Free rs')
- handle TERM _ => raise RecError "illegal argument in pattern";
- val lfrees = ls @ rs @ cargs;
-
- fun check_vars _ [] = ()
- | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
- in
- if length middle > 1 then
- raise RecError "more than one non-variable in pattern"
- else
- (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
- check_vars "extra variables on rhs: "
- (subtract (op =) lfrees (map dest_Free (OldTerm.term_frees rhs)));
- case AList.lookup (op =) rec_fns fnameT of
- NONE =>
- (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
- | SOME (_, rpos', eqns) =>
- if AList.defined (op =) eqns cname then
- raise RecError "constructor already occurred as pattern"
- else if rpos <> rpos' then
- raise RecError "position of recursive argument inconsistent"
- else
- AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
- rec_fns)
- end
- handle RecError s => primrec_eq_err thy s eq;
-
-fun process_fun thy descr rec_eqns (i, fnameT as (fname, _)) (fnameTs, fnss) =
- let
- val (_, (tname, _, constrs)) = List.nth (descr, i);
-
- (* substitute "fname ls x rs" by "y ls rs" for (x, (_, y)) in subs *)
-
- fun subst [] t fs = (t, fs)
- | subst subs (Abs (a, T, t)) fs =
- fs
- |> subst subs t
- |-> (fn t' => pair (Abs (a, T, t')))
- | subst subs (t as (_ $ _)) fs =
- let
- val (f, ts) = strip_comb t;
- in
- if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then
- let
- val fnameT' as (fname', _) = dest_Const f;
- val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
- val ls = take rpos ts;
- val rest = drop rpos ts;
- val (x', rs) = (hd rest, tl rest)
- handle Empty => raise RecError ("not enough arguments\
- \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
- val (x, xs) = strip_comb x'
- in case AList.lookup (op =) subs x
- of NONE =>
- fs
- |> fold_map (subst subs) ts
- |-> (fn ts' => pair (list_comb (f, ts')))
- | SOME (i', y) =>
- fs
- |> fold_map (subst subs) (xs @ ls @ rs)
- ||> process_fun thy descr rec_eqns (i', fnameT')
- |-> (fn ts' => pair (list_comb (y, ts')))
- end
- else
- fs
- |> fold_map (subst subs) (f :: ts)
- |-> (fn (f'::ts') => pair (list_comb (f', ts')))
- end
- | subst _ t fs = (t, fs);
-
- (* translate rec equations into function arguments suitable for rec comb *)
-
- fun trans eqns (cname, cargs) (fnameTs', fnss', fns) =
- (case AList.lookup (op =) eqns cname of
- NONE => (warning ("No equation for constructor " ^ quote cname ^
- "\nin definition of function " ^ quote fname);
- (fnameTs', fnss', (Const ("HOL.undefined", dummyT))::fns))
- | SOME (ls, cargs', rs, rhs, eq) =>
- let
- val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
- val rargs = map fst recs;
- val subs = map (rpair dummyT o fst)
- (rev (Term.rename_wrt_term rhs rargs));
- val (rhs', (fnameTs'', fnss'')) =
- (subst (map (fn ((x, y), z) =>
- (Free x, (body_index y, Free z)))
- (recs ~~ subs)) rhs (fnameTs', fnss'))
- handle RecError s => primrec_eq_err thy s eq
- in (fnameTs'', fnss'',
- (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
- end)
-
- in (case AList.lookup (op =) fnameTs i of
- NONE =>
- if exists (equal fnameT o snd) fnameTs then
- raise RecError ("inconsistent functions for datatype " ^ quote tname)
- else
- let
- val (_, _, eqns) = the (AList.lookup (op =) rec_eqns fnameT);
- val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs
- ((i, fnameT)::fnameTs, fnss, [])
- in
- (fnameTs', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
- end
- | SOME fnameT' =>
- if fnameT = fnameT' then (fnameTs, fnss)
- else raise RecError ("inconsistent functions for datatype " ^ quote tname))
- end;
-
-
-(* prepare functions needed for definitions *)
-
-fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
- case AList.lookup (op =) fns i of
- NONE =>
- let
- val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
- replicate (length cargs + length (filter is_rec_type cargs))
- dummyT ---> HOLogic.unitT)) constrs;
- val _ = warning ("No function definition for datatype " ^ quote tname)
- in
- (dummy_fns @ fs, defs)
- end
- | SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name, tname) :: defs);
-
-
-(* make definition *)
-
-fun make_def thy fs (fname, ls, rec_name, tname) =
- let
- val rhs = fold_rev (fn T => fn t => Abs ("", T, t))
- ((map snd ls) @ [dummyT])
- (list_comb (Const (rec_name, dummyT),
- fs @ map Bound (0 ::(length ls downto 1))))
- val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
- val def_prop =
- singleton (Syntax.check_terms (ProofContext.init_global thy))
- (Logic.mk_equals (Const (fname, dummyT), rhs));
- in (def_name, def_prop) end;
-
-
-(* find datatypes which contain all datatypes in tnames' *)
-
-fun find_dts (dt_info : info Symtab.table) _ [] = []
- | find_dts dt_info tnames' (tname::tnames) =
- (case Symtab.lookup dt_info tname of
- NONE => primrec_err (quote tname ^ " is not a datatype")
- | SOME dt =>
- if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
- (tname, dt)::(find_dts dt_info tnames' tnames)
- else find_dts dt_info tnames' tnames);
-
-fun prepare_induct ({descr, induct, ...}: info) rec_eqns =
- let
- fun constrs_of (_, (_, _, cs)) =
- map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
- val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
- in
- induct
- |> Rule_Cases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
- |> Rule_Cases.save induct
- end;
-
-local
-
-fun gen_primrec_i note def alt_name eqns_atts thy =
- let
- val (eqns, atts) = split_list eqns_atts;
- val dt_info = Datatype_Data.get_all thy;
- val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ;
- val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
- val dts = find_dts dt_info tnames tnames;
- val main_fns =
- map (fn (tname, {index, ...}) =>
- (index,
- (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
- dts;
- val {descr, rec_names, rec_rewrites, ...} =
- if null dts then
- primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
- else snd (hd dts);
- val (fnameTs, fnss) =
- fold_rev (process_fun thy descr rec_eqns) main_fns ([], []);
- val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
- val defs' = map (make_def thy fs) defs;
- val nameTs1 = map snd fnameTs;
- val nameTs2 = map fst rec_eqns;
- val _ = if eq_set (op =) (nameTs1, nameTs2) then ()
- else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
- "\nare not mutually recursive");
- val primrec_name =
- if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name;
- val (defs_thms', thy') =
- thy
- |> Sign.add_path primrec_name
- |> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
- val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';
- val simps = map (fn (_, t) => Goal.prove_global thy' [] [] t
- (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
- val (simps', thy'') =
- thy'
- |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
- val simps'' = maps snd simps';
- val lhss = map (Logic.varify_global o fst o Logic.dest_equals o snd) defs';
- in
- thy''
- |> note (("simps",
- [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
- |> snd
- |> Spec_Rules.add_global Spec_Rules.Equational (lhss, simps)
- |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
- |> snd
- |> Sign.parent_path
- |> pair simps''
- end;
-
-fun gen_primrec note def alt_name eqns thy =
- let
- val ((names, strings), srcss) = apfst split_list (split_list eqns);
- val atts = map (map (Attrib.attribute thy)) srcss;
- val eqn_ts = map (fn s => Syntax.read_prop_global thy s
- handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
- val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))
- handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
- val (_, eqn_ts') = unify_consts thy rec_ts eqn_ts
- in
- gen_primrec_i note def alt_name (names ~~ eqn_ts' ~~ atts) thy
- end;
-
-fun thy_note ((name, atts), thms) =
- Global_Theory.add_thmss [((Binding.name name, thms), atts)] #-> (fn [thms] => pair (name, thms));
-fun thy_def false ((name, atts), t) =
- Global_Theory.add_defs false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm))
- | thy_def true ((name, atts), t) =
- Global_Theory.add_defs_unchecked false [((Binding.name name, t), atts)] #-> (fn [thm] => pair (name, thm));
-
-in
-
-val add_primrec = gen_primrec thy_note (thy_def false);
-val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
-val add_primrec_i = gen_primrec_i thy_note (thy_def false);
-val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
-
-end;
-
-end;
--- a/src/HOL/Tools/primrec.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Wed Sep 29 17:59:20 2010 +0200
@@ -306,26 +306,12 @@
(* outer syntax *)
-val opt_unchecked_name =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!!
- (((Parse.$$$ "unchecked" >> K true) -- Scan.optional Parse.name "" ||
- Parse.name >> pair false) --| Parse.$$$ ")")) (false, "");
-
-val old_primrec_decl =
- opt_unchecked_name --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop);
-
val primrec_decl = Parse.opt_target -- Parse.fixes -- Parse_Spec.where_alt_specs;
val _ =
Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
Keyword.thy_decl
- ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
- Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
- || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
- Toplevel.theory (snd o
- (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
- alt_name (map Parse.triple_swap eqns) o
- tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
+ (primrec_decl >> (fn ((opt_target, fixes), specs) =>
+ Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)));
end;
--- a/src/HOL/ex/Fundefs.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy Wed Sep 29 17:59:20 2010 +0200
@@ -51,7 +51,7 @@
assumes trm: "nz_dom x"
shows "nz x = 0"
using trm
-by induct auto
+by induct (auto simp: nz.psimps)
termination nz
by (relation "less_than") (auto simp:nz_is_zero)
@@ -71,7 +71,7 @@
lemma f91_estimate:
assumes trm: "f91_dom n"
shows "n < f91 n + 11"
-using trm by induct auto
+using trm by induct (auto simp: f91.psimps)
termination
proof
--- a/src/HOL/ex/Unification.thy Wed Sep 29 17:58:27 2010 +0200
+++ b/src/HOL/ex/Unification.thy Wed Sep 29 17:59:20 2010 +0200
@@ -158,6 +158,7 @@
Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
by pat_completeness auto
+declare unify.psimps[simp]
subsection {* Partial correctness *}
@@ -533,4 +534,6 @@
qed
qed
+declare unify.psimps[simp del]
+
end
--- a/src/Provers/hypsubst.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/Provers/hypsubst.ML Wed Sep 29 17:59:20 2010 +0200
@@ -42,13 +42,10 @@
val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
val sym : thm (* a=b ==> b=a *)
val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *)
- val prop_subst : thm (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
end;
signature HYPSUBST =
sig
- val single_hyp_subst_tac : int -> int -> tactic
- val single_hyp_meta_subst_tac : int -> int -> tactic
val bound_hyp_subst_tac : int -> tactic
val hyp_subst_tac : int -> tactic
val blast_hyp_subst_tac : bool -> int -> tactic
@@ -61,27 +58,6 @@
exception EQ_VAR;
-val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)"
- by (unfold prop_def)}
-
-(** Simple version: Just subtitute one hypothesis, specified by index k **)
-fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
- let
- val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
- |> cterm_of (theory_of_cterm csubg)
-
- val rule =
- Thm.lift_rule pat subst_rule (* lift just over parameters *)
- |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
- in
- rotate_tac k i
- THEN Thm.compose_no_flatten false (rule, 1) i
- THEN rotate_tac (~k) i
- end)
-
-val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
-val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
-
fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
(*Simplifier turns Bound variables to special Free variables:
--- a/src/Tools/Code/code_scala.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Sep 29 17:59:20 2010 +0200
@@ -430,7 +430,7 @@
"true", "type", "val", "var", "while", "with", "yield"
]
#> fold (Code_Target.add_reserved target) [
- "apply", "error", "BigInt", "Nil", "List"
+ "apply", "error", "scala", "BigInt", "Nil", "List"
];
end; (*struct*)
--- a/src/Tools/Code/code_target.ML Wed Sep 29 17:58:27 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Sep 29 17:59:20 2010 +0200
@@ -55,7 +55,7 @@
val add_reserved: string -> string -> theory -> theory
val add_include: string -> string * (string * string list) option -> theory -> theory
- val codegen_tool: string (*theory name*) -> bool -> string (*export_code expr*) -> unit
+ val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
end;
structure Code_Target : CODE_TARGET =
@@ -692,10 +692,9 @@
(** external entrance point -- for codegen tool **)
-fun codegen_tool thyname qnd cmd_expr =
+fun codegen_tool thyname cmd_expr =
let
val thy = Thy_Info.get_theory thyname;
- val _ = quick_and_dirty := qnd;
val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
(filter Token.is_proper o Outer_Syntax.scan Position.none);
in case parse cmd_expr
--- a/src/Tools/Code/etc/settings Wed Sep 29 17:58:27 2010 +0200
+++ b/src/Tools/Code/etc/settings Wed Sep 29 17:59:20 2010 +0200
@@ -2,13 +2,13 @@
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
EXEC_GHC=$(choosefrom \
- "$ISABELLE_HOME/contrib/ghc" \
- "$ISABELLE_HOME/../ghc" \
+ "$ISABELLE_HOME/contrib/ghc/$ISABELLE_PLATFORM/ghc" \
+ "$ISABELLE_HOME/../ghc/$ISABELLE_PLATFORM/ghc" \
$(type -p ghc) \
"")
EXEC_OCAML=$(choosefrom \
- "$ISABELLE_HOME/contrib/ocaml" \
- "$ISABELLE_HOME/../ocaml" \
+ "$ISABELLE_HOME/contrib/ocaml/$ISABELLE_PLATFORM/ocaml" \
+ "$ISABELLE_HOME/../ocaml/$ISABELLE_PLATFORM/ocaml" \
$(type -p ocaml) \
"")
--- a/src/Tools/Code/lib/Tools/codegen Wed Sep 29 17:58:27 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Wed Sep 29 17:59:20 2010 +0200
@@ -55,9 +55,9 @@
handle _ => OS.Process.exit OS.Process.failure;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
- val qnd = $QUICK_AND_DIRTY; \
+ val _ = quick_and_dirty := $QUICK_AND_DIRTY; \
val cmd_expr = \"$CODE_EXPR\"; \
- val ml_cmd = \"Code_Target.codegen_tool thyname qnd cmd_expr\"; \
+ val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
$FORMAL_CMD"
"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1