updated generated files;
authorwenzelm
Sun Nov 07 23:12:21 2010 +0100 (2010-11-07)
changeset 40403e2721ac2a258
parent 40401 25ba6b2559e1
child 40404 c1cd5437afe8
updated generated files;
doc-src/Functions/Thy/document/Functions.tex
doc-src/TutorialI/Trie/document/Trie.tex
     1.1 --- a/doc-src/Functions/Thy/document/Functions.tex	Sun Nov 07 22:42:49 2010 +0100
     1.2 +++ b/doc-src/Functions/Thy/document/Functions.tex	Sun Nov 07 23:12:21 2010 +0100
     1.3 @@ -825,21 +825,7 @@
     1.4  \isakeyword{where}\isanewline
     1.5  \ \ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
     1.6  {\isacharbar}\ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
     1.7 -{\isacharbar}\ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ fib{\isadigit{2}}\ n\ {\isacharplus}\ fib{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
     1.8 -%
     1.9 -\isadelimML
    1.10 -%
    1.11 -\endisadelimML
    1.12 -%
    1.13 -\isatagML
    1.14 -%
    1.15 -\endisatagML
    1.16 -{\isafoldML}%
    1.17 -%
    1.18 -\isadelimML
    1.19 -%
    1.20 -\endisadelimML
    1.21 -%
    1.22 +{\isacharbar}\ {\isachardoublequoteopen}fib{\isadigit{2}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ fib{\isadigit{2}}\ n\ {\isacharplus}\ fib{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
    1.23  \isadelimproof
    1.24  %
    1.25  \endisadelimproof
    1.26 @@ -853,15 +839,7 @@
    1.27    either \isa{{\isadigit{0}}}, \isa{{\isadigit{1}}} or \isa{n\ {\isacharplus}\ {\isadigit{2}}}:
    1.28  
    1.29    \begin{isabelle}%
    1.30 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ x\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ x\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\isanewline
    1.31 -\ {\isadigit{2}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline
    1.32 -\ {\isadigit{3}}{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline
    1.33 -\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{0}}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
    1.34 -\ {\isadigit{5}}{\isachardot}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}\isanewline
    1.35 -\ {\isadigit{6}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{1}}\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ {\isadigit{1}}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
    1.36 -\ {\isadigit{7}}{\isachardot}\ {\isasymAnd}n\ na{\isachardot}\isanewline
    1.37 -\isaindent{\ {\isadigit{7}}{\isachardot}\ \ \ \ }n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ na\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
    1.38 -\isaindent{\ {\isadigit{7}}{\isachardot}\ \ \ \ }fib{\isadigit{2}}{\isacharunderscore}sumC\ n\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ na\ {\isacharplus}\ fib{\isadigit{2}}{\isacharunderscore}sumC\ {\isacharparenleft}Suc\ na{\isacharparenright}%
    1.39 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}P\ x{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ x\ {\isacharequal}\ {\isadigit{1}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ x\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
    1.40  \end{isabelle}
    1.41  
    1.42    This is an arithmetic triviality, but unfortunately the
    1.43 @@ -871,32 +849,6 @@
    1.44    Pattern compatibility and termination are automatic as usual.%
    1.45  \end{isamarkuptxt}%
    1.46  \isamarkuptrue%
    1.47 -%
    1.48 -\endisatagproof
    1.49 -{\isafoldproof}%
    1.50 -%
    1.51 -\isadelimproof
    1.52 -%
    1.53 -\endisadelimproof
    1.54 -%
    1.55 -\isadelimML
    1.56 -%
    1.57 -\endisadelimML
    1.58 -%
    1.59 -\isatagML
    1.60 -%
    1.61 -\endisatagML
    1.62 -{\isafoldML}%
    1.63 -%
    1.64 -\isadelimML
    1.65 -%
    1.66 -\endisadelimML
    1.67 -%
    1.68 -\isadelimproof
    1.69 -%
    1.70 -\endisadelimproof
    1.71 -%
    1.72 -\isatagproof
    1.73  \isacommand{apply}\isamarkupfalse%
    1.74  \ atomize{\isacharunderscore}elim\isanewline
    1.75  \isacommand{apply}\isamarkupfalse%
    1.76 @@ -1202,13 +1154,12 @@
    1.77  
    1.78    \noindent The hypothesis in our lemma was used to satisfy the first premise in
    1.79    the induction rule. However, we also get \isa{findzero{\isacharunderscore}dom\ {\isacharparenleft}f{\isacharcomma}\ n{\isacharparenright}} as a local assumption in the induction step. This
    1.80 -  allows to unfold \isa{findzero\ f\ n} using the \isa{psimps}
    1.81 -  rule, and the rest is trivial. Since the \isa{psimps} rules carry the
    1.82 -  \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute by default, we just need a single step:%
    1.83 +  allows unfolding \isa{findzero\ f\ n} using the \isa{psimps}
    1.84 +  rule, and the rest is trivial.%
    1.85  \end{isamarkuptxt}%
    1.86  \isamarkuptrue%
    1.87  \isacommand{apply}\isamarkupfalse%
    1.88 -\ simp\isanewline
    1.89 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ findzero{\isachardot}psimps{\isacharparenright}\isanewline
    1.90  \isacommand{done}\isamarkupfalse%
    1.91  %
    1.92  \endisatagproof
    1.93 @@ -1257,7 +1208,7 @@
    1.94  \ \ \ \ \isacommand{with}\isamarkupfalse%
    1.95  \ dom\ \isacommand{have}\isamarkupfalse%
    1.96  \ {\isachardoublequoteopen}findzero\ f\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    1.97 -\ simp\isanewline
    1.98 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ findzero{\isachardot}psimps{\isacharparenright}\isanewline
    1.99  \ \ \ \ \isacommand{with}\isamarkupfalse%
   1.100  \ x{\isacharunderscore}range\ \isacommand{show}\isamarkupfalse%
   1.101  \ False\ \isacommand{by}\isamarkupfalse%
   1.102 @@ -1286,7 +1237,7 @@
   1.103  \ \ \ \ \isacommand{with}\isamarkupfalse%
   1.104  \ dom\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
   1.105  \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharbraceleft}Suc\ n\ {\isachardot}{\isachardot}{\isacharless}\ findzero\ f\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   1.106 -\ simp\isanewline
   1.107 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ findzero{\isachardot}psimps{\isacharparenright}\isanewline
   1.108  \ \ \ \ \isacommand{with}\isamarkupfalse%
   1.109  \ IH\ \isakeyword{and}\ {\isacharbackquoteopen}f\ n\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
   1.110  \ \ \ \ \isacommand{show}\isamarkupfalse%
   1.111 @@ -1662,7 +1613,7 @@
   1.112  %
   1.113  \isatagproof
   1.114  \isacommand{by}\isamarkupfalse%
   1.115 -\ {\isacharparenleft}induct\ rule{\isacharcolon}nz{\isachardot}pinduct{\isacharparenright}\ auto%
   1.116 +\ {\isacharparenleft}induct\ rule{\isacharcolon}nz{\isachardot}pinduct{\isacharparenright}\ {\isacharparenleft}auto\ simp{\isacharcolon}\ nz{\isachardot}psimps{\isacharparenright}%
   1.117  \endisatagproof
   1.118  {\isafoldproof}%
   1.119  %
   1.120 @@ -1739,7 +1690,7 @@
   1.121  \isatagproof
   1.122  \isacommand{using}\isamarkupfalse%
   1.123  \ trm\ \isacommand{by}\isamarkupfalse%
   1.124 -\ induct\ auto%
   1.125 +\ induct\ {\isacharparenleft}auto\ simp{\isacharcolon}\ f{\isadigit{9}}{\isadigit{1}}{\isachardot}psimps{\isacharparenright}%
   1.126  \endisatagproof
   1.127  {\isafoldproof}%
   1.128  %
     2.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Sun Nov 07 22:42:49 2010 +0100
     2.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Sun Nov 07 23:12:21 2010 +0100
     2.3 @@ -208,7 +208,7 @@
     2.4    Conceptually, each node contains a mapping from letters to optional
     2.5    subtries. Above we have implemented this by means of an association
     2.6    list. Replay the development replacing \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list}
     2.7 -  with \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie}.
     2.8 +  with \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ option}.
     2.9  \end{exercise}%
    2.10  \end{isamarkuptext}%
    2.11  \isamarkuptrue%