# HG changeset patch # User wenzelm # Date 1285775960 -7200 # Node ID b1640def6d4450957b49146acd48eb53a108c957 # Parent 533dd8cda12c18548d9580e463bfeef5ef027c12# Parent b59e064e32c3013b31457e8919a00c6f3b428f8c merged diff -r b59e064e32c3 -r b1640def6d44 NEWS --- 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. diff -r b59e064e32c3 -r b1640def6d44 doc-src/Classes/IsaMakefile --- 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 diff -r b59e064e32c3 -r b1640def6d44 doc-src/Classes/Thy/Classes.thy --- 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)} *} diff -r b59e064e32c3 -r b1640def6d44 doc-src/Classes/Thy/document/Classes.tex --- 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% } diff -r b59e064e32c3 -r b1640def6d44 doc-src/Classes/style.sty --- 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} diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/IsaMakefile --- 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 diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/Adaptation.thy --- 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 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 \" +code_const %quotett True and False and "op \" (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 \" +code_const %quotett "op \" (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 diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/Evaluation.thy --- 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)) = diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/Foundations.thy --- 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)} *} diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/Further.thy --- 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)} *} diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/Introduction.thy --- 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)} *} diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/Refinement.thy --- 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 *) diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/document/Adaptation.tex --- 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 diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/document/Evaluation.tex --- 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; diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/document/Foundations.tex --- 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 diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/document/Further.tex --- 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% } diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/document/Introduction.tex --- 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.% diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/Thy/document/Refinement.tex --- 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 diff -r b59e064e32c3 -r b1640def6d44 doc-src/Codegen/style.sty --- 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} diff -r b59e064e32c3 -r b1640def6d44 doc-src/Functions/IsaMakefile --- 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 diff -r b59e064e32c3 -r b1640def6d44 doc-src/Functions/Thy/Functions.thy --- 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 \ 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 \ 0` show ?thesis by simp next assume "x \ {Suc n ..< findzero f n}" - with dom and `f n \ 0` have "x \ {Suc n ..< findzero f (Suc n)}" by simp + with dom and `f n \ 0` have "x \ {Suc n ..< findzero f (Suc n)}" by (simp add: findzero.psimps) with IH and `f n \ 0` show ?thesis by simp qed @@ -1071,7 +1068,7 @@ *} (*<*)oops(*>*) lemma nz_is_zero: "nz_dom n \ 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 diff -r b59e064e32c3 -r b1640def6d44 src/FOL/hypsubstdata.ML --- 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); diff -r b59e064e32c3 -r b1640def6d44 src/HOL/HOL.thy --- 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; diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Imperative_HOL/Mrec.thy --- 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 \ None) | None \ 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Inductive.thy --- 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: *} diff -r b59e064e32c3 -r b1640def6d44 src/HOL/IsaMakefile --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Library/Code_Natural.thy --- 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) diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Library/Efficient_Nat.thy --- 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) diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Library/Kleene_Algebra.thy --- 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 "\x. 0", tailrec, domintros) - mk_tcl :: "('a::{plus,times,ord,zero}) \ 'a \ 'a" -where - "mk_tcl A X = (if X * A \ 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 \ 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 \ X \ 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 \ mk_tcl_dom x" - by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases) - -lemma mk_tcl_default: "\ mk_tcl_dom (a,x) \ 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 \ 0" - shows "mk_tcl A A = tcl A" - using assms mk_tcl_default mk_tcl_correctness - unfolding tcl_def - by auto - -end diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Library/More_List.thy --- 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 (\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 \ set xs" "y \ set xs" with assms have *: "f y = f x \ y = x" by (auto dest: inj_onD) + have **: "x = y \ y = x" by auto show "(insort_key f y \ insort_key f x) zs = (insort_key f x \ 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/List.thy --- 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 \ 'a" where - "listsum [] = 0" - | "listsum (x # xs) = x + listsum xs" + "listsum xs = foldr plus xs 0" primrec drop:: "nat \ 'a list \ '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\'a::monoid_add)" -by (induct xs arbitrary: a) (auto simp:add_assoc) - -corollary foldl_foldr1: - "foldl op + 0 xs = foldr op + xs (0\'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 \ foldl (op +) n ns"} looks simpler, but is more @@ -2869,56 +2871,57 @@ subsubsection {* List summation: @{const listsum} and @{text"\"}*} -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\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 \ ('b::comm_monoid_add)" -shows "x : set xs \ 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 \ set xs \ 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 \ 'b \ comm_monoid_add" - assumes "\ x. \ x \ set xs ; \ P x \ \ 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 "\x. x \ set xs \ \ P x \ 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 \ listsum xs = Setsum(set xs)" -by (induct xs) simp_all - -lemma listsum_eq_0_nat_iff_nat[simp]: - "listsum ns = (0::nat) \ (\ n \ set ns. n = 0)" -by(simp add: listsum) - -lemma elem_le_listsum_nat: "k ns!k <= listsum(ns::nat list)" + using assms by (induct xs) auto + +lemma (in monoid_add) distinct_listsum_conv_Setsum: + "distinct xs \ listsum xs = Setsum (set xs)" + by (induct xs) simp_all + +lemma listsum_eq_0_nat_iff_nat [simp]: + "listsum ns = (0::nat) \ (\n \ set ns. n = 0)" + by (simp add: listsum_foldl) + +lemma elem_le_listsum_nat: + "k < size ns \ ns ! k \ 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 - listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k" +lemma listsum_update_nat: + "k 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)" "\x\xs. b" == "CONST listsum (CONST map (%x. b) xs)" -lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r" +lemma (in monoid_add) listsum_triv: + "(\x\xs. r) = of_nat (length xs) * r" by (induct xs) (simp_all add: left_distrib) -lemma listsum_0 [simp]: "(\x\xs. 0) = 0" +lemma (in monoid_add) listsum_0 [simp]: + "(\x\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 \ 'b\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 \ 'b::comm_monoid_add" - shows "(\x\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 \ 'b::ab_group_add" - shows "(\x\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 \ 'b::semiring_0" - shows "(\x\xs. c * f x) = c * (\x\xs. f x)" -by (induct xs, simp_all add: algebra_simps) - -lemma listsum_mult_const: - fixes f :: "'a \ 'b::semiring_0" - shows "(\x\xs. f x * c) = (\x\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 "\listsum xs\ \ 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 \ f) xs)" + by (induct xs) simp_all + +lemma (in comm_monoid_add) listsum_addf: + "(\x\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: + "(\x\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: + "(\x\xs. c * f x) = c * (\x\xs. f x)" + by (induct xs) (simp_all add: algebra_simps) + +lemma (in semiring_0) listsum_mult_const: + "(\x\xs. f x * c) = (\x\xs. f x) * c" + by (induct xs) (simp_all add: algebra_simps) + +lemma (in ordered_ab_group_add_abs) listsum_abs: + "\listsum xs\ \ listsum (map abs xs)" + by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq]) lemma listsum_mono: - fixes f g :: "'a \ 'b::{comm_monoid_add, ordered_ab_semigroup_add}" + fixes f g :: "'a \ 'b::{monoid_add, ordered_ab_semigroup_add}" shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\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 \ 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.. i = 0 ..< length xs. xs ! i)" using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth) diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy --- 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 \ nat \ bool) \ nat \ 'a list \ bool" -primrec + +primrec list_all'_rec :: "('a \ nat \ bool) \ nat \ 'a list \ bool" +where "list_all'_rec P n [] = True" - "list_all'_rec P n (x#xs) = (P x n \ list_all'_rec P (Suc n) xs)" +| "list_all'_rec P n (x#xs) = (P x n \ list_all'_rec P (Suc n) xs)" definition list_all' :: "('a \ nat \ bool) \ 'a list \ bool" where "list_all' P xs \ list_all'_rec P 0 xs" diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/Comp/TranslComp.thy --- 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); diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/Comp/TranslCompTp.thy --- 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 \ state_type \ state_type" where "sttp_of == snd" -consts - compTpExpr :: "java_mb \ java_mb prog \ expr - \ state_type \ method_type \ state_type" - - compTpExprs :: "java_mb \ java_mb prog \ expr list - \ state_type \ method_type \ state_type" - - compTpStmt :: "java_mb \ java_mb prog \ stmt - \ state_type \ method_type \ state_type" - definition nochangeST :: "state_type \ method_type \ state_type" where "nochangeST sttp == ([Some sttp], sttp)" @@ -80,60 +70,45 @@ (* Expressions *) -primrec - +primrec compTpExpr :: "java_mb \ java_mb prog \ expr \ + state_type \ method_type \ state_type" + and compTpExprs :: "java_mb \ java_mb prog \ expr list \ + state_type \ method_type \ state_type" +where "compTpExpr jmb G (NewC c) = pushST [Class c]" - - "compTpExpr jmb G (Cast c e) = - (compTpExpr jmb G e) \ (replST 1 (Class c))" - - "compTpExpr jmb G (Lit val) = pushST [the (typeof (\v. None) val)]" - - "compTpExpr jmb G (BinOp bo e1 e2) = +| "compTpExpr jmb G (Cast c e) = (compTpExpr jmb G e) \ (replST 1 (Class c))" +| "compTpExpr jmb G (Lit val) = pushST [the (typeof (\v. None) val)]" +| "compTpExpr jmb G (BinOp bo e1 e2) = (compTpExpr jmb G e1) \ (compTpExpr jmb G e2) \ (case bo of Eq => popST 2 \ pushST [PrimT Boolean] \ popST 1 \ pushST [PrimT Boolean] | Add => replST 2 (PrimT Integer))" - - "compTpExpr jmb G (LAcc vn) = (\ (ST, LT). +| "compTpExpr jmb G (LAcc vn) = (\ (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) \ dupST \ (popST 1)" - - - "compTpExpr jmb G ( {cn}e..fn ) = +| "compTpExpr jmb G ( {cn}e..fn ) = (compTpExpr jmb G e) \ 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) \ (compTpExpr jmb G e2) \ dup_x1ST \ (popST 2)" - - - "compTpExpr jmb G ({C}a..mn({fpTs}ps)) = +| "compTpExpr jmb G ({C}a..mn({fpTs}ps)) = (compTpExpr jmb G a) \ (compTpExprs jmb G ps) \ (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) \ (compTpExprs jmb G es)" +| "compTpExprs jmb G [] = comb_nil" +| "compTpExprs jmb G (e#es) = (compTpExpr jmb G e) \ (compTpExprs jmb G es)" (* Statements *) -primrec - "compTpStmt jmb G Skip = comb_nil" - - "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) \ popST 1" - - "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \ (compTpStmt jmb G c2)" - - "compTpStmt jmb G (If(e) c1 Else c2) = +primrec compTpStmt :: "java_mb \ java_mb prog \ stmt \ + state_type \ method_type \ state_type" +where + "compTpStmt jmb G Skip = comb_nil" +| "compTpStmt jmb G (Expr e) = (compTpExpr jmb G e) \ popST 1" +| "compTpStmt jmb G (c1;; c2) = (compTpStmt jmb G c1) \ (compTpStmt jmb G c2)" +| "compTpStmt jmb G (If(e) c1 Else c2) = (pushST [PrimT Boolean]) \ (compTpExpr jmb G e) \ popST 2 \ (compTpStmt jmb G c1) \ nochangeST \ (compTpStmt jmb G c2)" - - "compTpStmt jmb G (While(e) c) = +| "compTpStmt jmb G (While(e) c) = (pushST [PrimT Boolean]) \ (compTpExpr jmb G e) \ popST 2 \ (compTpStmt jmb G c) \ nochangeST" @@ -141,13 +116,11 @@ \ state_type \ method_type \ state_type" where "compTpInit jmb == (\ (vn,ty). (pushST [ty]) \ (storeST (index jmb vn) ty))" -consts - compTpInitLvars :: "[java_mb, (vname \ ty) list] - \ state_type \ method_type \ state_type" - -primrec +primrec compTpInitLvars :: "[java_mb, (vname \ ty) list] \ + state_type \ method_type \ state_type" +where "compTpInitLvars jmb [] = comb_nil" - "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \ (compTpInitLvars jmb lvars)" +| "compTpInitLvars jmb (lv#lvars) = (compTpInit jmb lv) \ (compTpInitLvars jmb lvars)" definition start_ST :: "opstack_type" where "start_ST == []" diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/DFA/Err.thy --- 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 \ 'b err) \ ('a err \ 'b err)" -primrec +primrec strict :: "('a \ 'b err) \ ('a err \ '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) = (\ z. x = OK z \ f z = OK y)" diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/J/Value.thy --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/J/WellType.thy --- 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]: "(\a. v \ Addr a) --> (\T. typeof t v = Some T \ is_type G T)" diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/JVM/JVMExceptions.thy --- 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 \ pc < end_pc \ G\ cn \C catch_type" -consts - match_exception_table :: "jvm_prog \ cname \ p_count \ exception_table - \ p_count option" -primrec +primrec match_exception_table :: "jvm_prog \ cname \ p_count \ exception_table + \ 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 \ val option \ aheap \ frame list \ jvm_state" -primrec +primrec find_handler :: "jvm_prog \ val option \ aheap \ frame list + \ 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 \ (None, hp, fr#frs) | Some xc \ diff -r b59e064e32c3 -r b1640def6d44 src/HOL/MicroJava/JVM/JVMExecInstr.thy --- 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 \ (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 \ (oc, fs((F,C) \ 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; diff -r b59e064e32c3 -r b1640def6d44 src/HOL/NanoJava/Example.thy --- 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 \ val \ nat \ bool" ("_:_ \ _" [51, 51, 51] 50) -primrec "s:x\0 = (x\Null)" - "s:x\Suc n = (\a. x=Addr a \ heap s a \ None \ s:get_field s a pred\n)" +primrec Nat_atleast :: "state \ val \ nat \ bool" ("_:_ \ _" [51, 51, 51] 50) where + "s:x\0 = (x\Null)" +| "s:x\Suc n = (\a. x=Addr a \ heap s a \ None \ s:get_field s a pred\n)" lemma Nat_atleast_lupd [rule_format, simp]: "\s v::val. lupd(x\y) s:v \ n = (s:v \ n)" diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Nominal/Examples/Standardization.thy --- 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 "\y::name. y \ (x, u, z)") prefer 2 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Nominal/Nominal.thy --- 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" (************************************************************) diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Nominal/old_primrec.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; diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/SET_Protocol/Cardholder_Registration.thy --- 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 => - ((\N X Y. A \ Spy & + "KeyCryptKey DK K (ev # evs) = + (KeyCryptKey DK K evs | + (case ev of + Says A B Z => + ((\N X Y. A \ Spy & DK \ symKeys & Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) | - (\C. DK = priEK C)) - | Gets A' X => False - | Notes A' X => False))" + (\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; diff -r b59e064e32c3 -r b1640def6d44 src/HOL/SET_Protocol/Event_SET.thy --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/SET_Protocol/Public_SET.thy --- 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 \ "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*} diff -r b59e064e32c3 -r b1640def6d44 src/HOL/SET_Protocol/ROOT.ML --- 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"]; diff -r b59e064e32c3 -r b1640def6d44 src/HOL/SET_Protocol/SET_Protocol.thy --- /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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Datatype/datatype_selectors.ML --- 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) diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Function/function.ML --- 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 "_" diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Function/function_lib.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Function/induction_schema.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Function/mutual.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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) = diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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 => diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/hologic.ML --- 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 *) diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/old_primrec.ML --- 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; diff -r b59e064e32c3 -r b1640def6d44 src/HOL/Tools/primrec.ML --- 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; diff -r b59e064e32c3 -r b1640def6d44 src/HOL/ex/Fundefs.thy --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/HOL/ex/Unification.thy --- 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 \ \ Some (\ \ \)))" by pat_completeness auto +declare unify.psimps[simp] subsection {* Partial correctness *} @@ -533,4 +534,6 @@ qed qed +declare unify.psimps[simp del] + end diff -r b59e064e32c3 -r b1640def6d44 src/Provers/hypsubst.ML --- 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 \ PROP prop (x \ t \ 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: diff -r b59e064e32c3 -r b1640def6d44 src/Tools/Code/code_scala.ML --- 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*) diff -r b59e064e32c3 -r b1640def6d44 src/Tools/Code/code_target.ML --- 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 diff -r b59e064e32c3 -r b1640def6d44 src/Tools/Code/etc/settings --- 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) \ "") diff -r b59e064e32c3 -r b1640def6d44 src/Tools/Code/lib/Tools/codegen --- 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