ProgTutorial/Intro.thy
changeset 565 cecd7a941885
parent 560 8d30446d89f0
child 567 f7c97e64cc2a
equal deleted inserted replaced
564:6e2479089226 565:cecd7a941885
     1 theory Intro
     1 theory Intro
     2 imports Base
     2 imports Base
     3 begin
     3 begin
     4 
     4 
     5 chapter {* Introduction *}
     5 chapter \<open>Introduction\<close>
     6 
     6 
     7 
     7 
     8 text {*
     8 text \<open>
     9    \begin{flushright}
     9    \begin{flushright}
    10   {\em
    10   {\em
    11   ``My thesis is that programming is not at the bottom of the intellectual \\
    11   ``My thesis is that programming is not at the bottom of the intellectual \\
    12   pyramid, but at the top. It's creative design of the highest order. It \\
    12   pyramid, but at the top. It's creative design of the highest order. It \\
    13   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
    13   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
    35   please let us know. It is impossible for us to know every environment,
    35   please let us know. It is impossible for us to know every environment,
    36   operating system or editor in which Isabelle is used. If you have comments,
    36   operating system or editor in which Isabelle is used. If you have comments,
    37   criticism or like to add to the tutorial, please feel free---you are most
    37   criticism or like to add to the tutorial, please feel free---you are most
    38   welcome!! The tutorial is meant to be gentle and comprehensive. To achieve
    38   welcome!! The tutorial is meant to be gentle and comprehensive. To achieve
    39   this we need your help and feedback.
    39   this we need your help and feedback.
    40 *}
    40 \<close>
    41 
    41 
    42 section {* Intended Audience and Prior Knowledge *}
    42 section \<open>Intended Audience and Prior Knowledge\<close>
    43 
    43 
    44 text {* 
    44 text \<open>
    45   This tutorial targets readers who already know how to use Isabelle for
    45   This tutorial targets readers who already know how to use Isabelle for
    46   writing theories and proofs. We also assume that readers are familiar with
    46   writing theories and proofs. We also assume that readers are familiar with
    47   the functional programming language ML, the language in which most of
    47   the functional programming language ML, the language in which most of
    48   Isabelle is implemented. If you are unfamiliar with either of these two
    48   Isabelle is implemented. If you are unfamiliar with either of these two
    49   subjects, then you should first work through the Isabelle/HOL tutorial
    49   subjects, then you should first work through the Isabelle/HOL tutorial
    50   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently,
    50   \cite{isa-tutorial} or Paulson's book on ML \cite{paulson-ml2}. Recently,
    51   Isabelle has adopted a sizable amount of Scala code for a slick GUI
    51   Isabelle has adopted a sizable amount of Scala code for a slick GUI
    52   based on jEdit. This part of the code is beyond the interest of this
    52   based on jEdit. This part of the code is beyond the interest of this
    53   tutorial, since it mostly does not concern the regular Isabelle 
    53   tutorial, since it mostly does not concern the regular Isabelle 
    54   developer.
    54   developer.
    55 *}
    55 \<close>
    56 
    56 
    57 section {* Existing Documentation *}
    57 section \<open>Existing Documentation\<close>
    58 
    58 
    59 text {*
    59 text \<open>
    60   The following documentation about Isabelle programming already exists (and is
    60   The following documentation about Isabelle programming already exists (and is
    61   part of the distribution of Isabelle):
    61   part of the distribution of Isabelle):
    62 
    62 
    63   \begin{description}
    63   \begin{description}
    64   \item[The Isabelle/Isar Implementation Manual] describes Isabelle
    64   \item[The Isabelle/Isar Implementation Manual] describes Isabelle
    84   code is uncommented, some parts have very helpful comments---particularly
    84   code is uncommented, some parts have very helpful comments---particularly
    85   the code about theorems and terms. Despite the lack of comments in most
    85   the code about theorems and terms. Despite the lack of comments in most
    86   parts, it is often good to look at code that does similar things as you 
    86   parts, it is often good to look at code that does similar things as you 
    87   want to do and learn from it. 
    87   want to do and learn from it. 
    88   This tutorial contains frequently pointers to the
    88   This tutorial contains frequently pointers to the
    89   Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
    89   Isabelle sources. Still, the UNIX command \mbox{\<open>grep -R\<close>} is
    90   often your best friend while programming with Isabelle.\footnote{Or
    90   often your best friend while programming with Isabelle.\footnote{Or
    91   hypersearch if you work with jEdit.} To understand the sources,
    91   hypersearch if you work with jEdit.} To understand the sources,
    92   it is often also necessary to track the change history of a file or
    92   it is often also necessary to track the change history of a file or
    93   files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} 
    93   files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}} 
    94   for Isabelle  provides convenient interfaces to query the history of
    94   for Isabelle  provides convenient interfaces to query the history of
    95   files and ``change sets''.
    95   files and ``change sets''.
    96   \end{description}
    96   \end{description}
    97 *}
    97 \<close>
    98 
    98 
    99 section {* Typographic Conventions *}
    99 section \<open>Typographic Conventions\<close>
   100 
   100 
   101 text {*
   101 text \<open>
   102   All ML-code in this tutorial is typeset in shaded boxes, like the following 
   102   All ML-code in this tutorial is typeset in shaded boxes, like the following 
   103   simple ML-expression:
   103   simple ML-expression:
   104 
   104 
   105   \begin{isabelle}
   105   \begin{isabelle}
   106   \begin{graybox}
   106   \begin{graybox}
   107   \isacommand{ML}~@{text "\<verbopen>"}\isanewline
   107   \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
   108   \hspace{5mm}@{ML "3 + 4"}\isanewline
   108   \hspace{5mm}@{ML "3 + 4"}\isanewline
   109   @{text "\<verbclose>"}
   109   \<open>\<verbclose>\<close>
   110   \end{graybox}
   110   \end{graybox}
   111   \end{isabelle}
   111   \end{isabelle}
   112   
   112   
   113   These boxes correspond to how code can be processed inside the interactive
   113   These boxes correspond to how code can be processed inside the interactive
   114   environment of Isabelle. It is therefore easy to experiment with the code
   114   environment of Isabelle. It is therefore easy to experiment with the code
   115   that is shown in this tutorial. However, for better readability we will drop
   115   that is shown in this tutorial. However, for better readability we will drop
   116   the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just
   116   the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just
   117   write:
   117   write:
   118 
   118 
   119   @{ML [display,gray] "3 + 4"}
   119   @{ML [display,gray] "3 + 4"}
   120   
   120   
   121   Whenever appropriate we also show the response the code 
   121   Whenever appropriate we also show the response the code 
   124 
   124 
   125   @{ML_response [display,gray] "3 + 4" "7"}
   125   @{ML_response [display,gray] "3 + 4" "7"}
   126 
   126 
   127   The user-level commands of Isabelle (i.e., the non-ML code) are written
   127   The user-level commands of Isabelle (i.e., the non-ML code) are written
   128   in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
   128   in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
   129   \isacommand{foobar} and so on).  We use @{text "$ \<dots>"} to indicate that a
   129   \isacommand{foobar} and so on).  We use \<open>$ \<dots>\<close> to indicate that a
   130   command needs to be run in a UNIX-shell, for example:
   130   command needs to be run in a UNIX-shell, for example:
   131 
   131 
   132   @{text [display] "$ grep -R Thy_Output *"}
   132   @{text [display] "$ grep -R Thy_Output *"}
   133 
   133 
   134   Pointers to further information and Isabelle files are typeset in 
   134   Pointers to further information and Isabelle files are typeset in 
   144   of Isabelle.
   144   of Isabelle.
   145 
   145 
   146   A few exercises are scattered around the text. Their solutions are given 
   146   A few exercises are scattered around the text. Their solutions are given 
   147   in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
   147   in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
   148   to solve the exercises on your own, and then look at the solutions.
   148   to solve the exercises on your own, and then look at the solutions.
   149 *}
   149 \<close>
   150 
   150 
   151 section {* How To Understand Isabelle Code *}
   151 section \<open>How To Understand Isabelle Code\<close>
   152 
   152 
   153 text {*
   153 text \<open>
   154   One of the more difficult aspects of any kind of programming is to
   154   One of the more difficult aspects of any kind of programming is to
   155   understand code written by somebody else. This is aggravated in Isabelle by
   155   understand code written by somebody else. This is aggravated in Isabelle by
   156   the fact that many parts of the code contain none or only few
   156   the fact that many parts of the code contain none or only few
   157   comments. There is one strategy that might be helpful to navigate your way:
   157   comments. There is one strategy that might be helpful to navigate your way:
   158   ML is an interactive programming environment, which means you can evaluate
   158   ML is an interactive programming environment, which means you can evaluate
   159   code on the fly (for example inside an \isacommand{ML}~@{text
   159   code on the fly (for example inside an \isacommand{ML}~\<open>\<verbopen>\<dots>\<verbclose>\<close> section). So you can copy (self-contained)
   160   "\<verbopen>\<dots>\<verbclose>"} section). So you can copy (self-contained)
       
   161   chunks of existing code into a separate theory file and then study it
   160   chunks of existing code into a separate theory file and then study it
   162   alongside with examples. You can also install ``probes'' inside the copied
   161   alongside with examples. You can also install ``probes'' inside the copied
   163   code without having to recompile the whole Isabelle distribution. Such
   162   code without having to recompile the whole Isabelle distribution. Such
   164   probes might be messages or printouts of variables (see chapter
   163   probes might be messages or printouts of variables (see chapter
   165   \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
   164   \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
   166   probing the code with explicit print statements is the most effective method
   165   probing the code with explicit print statements is the most effective method
   167   for understanding what some piece of code is doing. However do not expect
   166   for understanding what some piece of code is doing. However do not expect
   168   quick results with this! It is painful. Depending on the size of the code
   167   quick results with this! It is painful. Depending on the size of the code
   169   you are looking at, you will spend the better part of a quiet afternoon with
   168   you are looking at, you will spend the better part of a quiet afternoon with
   170   it. And there seems to be no better way for understanding code in Isabelle.
   169   it. And there seems to be no better way for understanding code in Isabelle.
   171 *}
   170 \<close>
   172 
   171 
   173 
   172 
   174 section {* Aaaaargh! My Code Does not Work Anymore *}
   173 section \<open>Aaaaargh! My Code Does not Work Anymore\<close>
   175 
   174 
   176 text {*
   175 text \<open>
   177   One unpleasant aspect of any code development inside a larger system is that
   176   One unpleasant aspect of any code development inside a larger system is that
   178   one has to aim at a ``moving target''. Isabelle is no exception of this. Every 
   177   one has to aim at a ``moving target''. Isabelle is no exception of this. Every 
   179   update lets potentially all hell break loose, because other developers have
   178   update lets potentially all hell break loose, because other developers have
   180   changed code you are relying on. Cursing is somewhat helpful in such situations, 
   179   changed code you are relying on. Cursing is somewhat helpful in such situations, 
   181   but taking the view that incompatible code changes are a fact of life 
   180   but taking the view that incompatible code changes are a fact of life 
   206   problem with updating your code after submission. At the moment developers
   205   problem with updating your code after submission. At the moment developers
   207   are not as diligent with checking their code against the AFP than with
   206   are not as diligent with checking their code against the AFP than with
   208   checking agains the distribution, but generally problems will be caught and
   207   checking agains the distribution, but generally problems will be caught and
   209   the developer, who caused them, is expected to fix them. So also in this
   208   the developer, who caused them, is expected to fix them. So also in this
   210   case code maintenance is done for you.
   209   case code maintenance is done for you.
   211 *}
   210 \<close>
   212 
   211 
   213 section {* Serious Isabelle ML-Programming *}
   212 section \<open>Serious Isabelle ML-Programming\<close>
   214 
   213 
   215 text {*
   214 text \<open>
   216   As already pointed out in the previous section, Isabelle is a joint effort 
   215   As already pointed out in the previous section, Isabelle is a joint effort 
   217   of many developers. Therefore, disruptions that break the work of others
   216   of many developers. Therefore, disruptions that break the work of others
   218   are generally frowned upon. ``Accidents'' however do happen and everybody knows
   217   are generally frowned upon. ``Accidents'' however do happen and everybody knows
   219   this. Still to keep them to a minimum, you can submit your changes first to a rather 
   218   this. Still to keep them to a minimum, you can submit your changes first to a rather 
   220   sophisticated \emph{testboard}, which will perform checks of your changes against the
   219   sophisticated \emph{testboard}, which will perform checks of your changes against the
   234 
   233 
   235   @{text [display] "$ hg push -f ssh://...@hgbroy.informatik.tu-muenchen.de\\
   234   @{text [display] "$ hg push -f ssh://...@hgbroy.informatik.tu-muenchen.de\\
   236    //home/isabelle-repository/repos/testboard"}
   235    //home/isabelle-repository/repos/testboard"}
   237 
   236 
   238   where the dots need to be replaced by your login name.  Note that for
   237   where the dots need to be replaced by your login name.  Note that for
   239   pushing changes to the testboard you need to add the option @{text "-f"},
   238   pushing changes to the testboard you need to add the option \<open>-f\<close>,
   240   which should \emph{never} be used with the main Isabelle
   239   which should \emph{never} be used with the main Isabelle
   241   repository. While the testboard is a great system for supporting Isabelle
   240   repository. While the testboard is a great system for supporting Isabelle
   242   developers, its disadvantage is that it needs login permissions for the
   241   developers, its disadvantage is that it needs login permissions for the
   243   computers in Munich. So in order to use it, you might have to ask other
   242   computers in Munich. So in order to use it, you might have to ask other
   244   developers to obtain one.
   243   developers to obtain one.
   245 *}
   244 \<close>
   246 
   245 
   247 
   246 
   248 section {* Some Naming Conventions in the Isabelle Sources *}
   247 section \<open>Some Naming Conventions in the Isabelle Sources\<close>
   249 
   248 
   250 text {*
   249 text \<open>
   251   There are a few naming conventions in the Isabelle code that might aid reading 
   250   There are a few naming conventions in the Isabelle code that might aid reading 
   252   and writing code. (Remember that code is written once, but read many 
   251   and writing code. (Remember that code is written once, but read many 
   253   times.) The most important conventions are:
   252   times.) The most important conventions are:
   254 
   253 
   255   \begin{itemize}
   254   \begin{itemize}
   256   \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
   255   \item \<open>t\<close>, \<open>u\<close>, \<open>trm\<close> for (raw) terms; ML-type: @{ML_type term}
   257   \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
   256   \item \<open>ct\<close>, \<open>cu\<close> for certified terms; ML-type: @{ML_type cterm}
   258   \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
   257   \item \<open>ty\<close>, \<open>T\<close>, \<open>U\<close> for (raw) types; ML-type: @{ML_type typ}
   259   \item @{text "S"} for sorts; ML-type: @{ML_type sort}
   258   \item \<open>S\<close> for sorts; ML-type: @{ML_type sort}
   260   \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
   259   \item \<open>th\<close>, \<open>thm\<close> for theorems; ML-type: @{ML_type thm}
   261   \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
   260   \item \<open>foo_tac\<close> for tactics; ML-type: @{ML_type tactic}
   262   \item @{text thy} for theories; ML-type: @{ML_type theory}
   261   \item \<open>thy\<close> for theories; ML-type: @{ML_type theory}
   263   \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context}
   262   \item \<open>ctxt\<close> for proof contexts; ML-type: @{ML_type Proof.context}
   264   \item @{text lthy} for local theories; ML-type: @{ML_type local_theory}
   263   \item \<open>lthy\<close> for local theories; ML-type: @{ML_type local_theory}
   265   \item @{text context} for generic contexts; ML-type @{ML_type Context.generic}
   264   \item \<open>context\<close> for generic contexts; ML-type @{ML_type Context.generic}
   266   \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix}
   265   \item \<open>mx\<close> for mixfix syntax annotations; ML-type @{ML_type mixfix}
   267   \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T}
   266   \item \<open>prt\<close> for pretty printing; ML-type @{ML_type Pretty.T}
   268   \item @{text phi} for morphisms; ML-type @{ML_type morphism}
   267   \item \<open>phi\<close> for morphisms; ML-type @{ML_type morphism}
   269   \end{itemize}
   268   \end{itemize}
   270 *}
   269 \<close>
   271 
   270 
   272 section {* Acknowledgements *}
   271 section \<open>Acknowledgements\<close>
   273 
   272 
   274 text {*
   273 text \<open>
   275   Financial support for this tutorial was provided by the German 
   274   Financial support for this tutorial was provided by the German 
   276   Research Council (DFG) under grant number URB 165/5-1. The following
   275   Research Council (DFG) under grant number URB 165/5-1. The following
   277   people contributed to the text:
   276   people contributed to the text:
   278 
   277 
   279   \begin{itemize}
   278   \begin{itemize}
   280   \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
   279   \item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
   281   \simpleinductive-package and the code for the @{text
   280   \simpleinductive-package and the code for the \<open>chunk\<close>-antiquotation. He also wrote the first version of chapter
   282   "chunk"}-antiquotation. He also wrote the first version of chapter
       
   283   \ref{chp:package} describing this package and has been helpful \emph{beyond
   281   \ref{chp:package} describing this package and has been helpful \emph{beyond
   284   measure} with answering questions about Isabelle.
   282   measure} with answering questions about Isabelle.
   285 
   283 
   286   \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}
   284   \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}
   287   and exercise \ref{fun:killqnt}.
   285   and exercise \ref{fun:killqnt}.
   288 
   286 
   289   \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, 
   287   \item {\bf Sascha B�hme} contributed the recipes in \ref{rec:timeout}, 
   290   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 
   288   \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} 
   291   and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
   289   and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
   292   are by him.
   290   are by him.
   293 
   291 
   294   \item {\bf Lukas Bulwahn} made me aware of a problem with recursive
   292   \item {\bf Lukas Bulwahn} made me aware of a problem with recursive
   318 
   316 
   319   \item {\bf Christian Sternagel} proofread the tutorial and made 
   317   \item {\bf Christian Sternagel} proofread the tutorial and made 
   320   many improvemets to the text. 
   318   many improvemets to the text. 
   321 
   319 
   322   \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation 
   320   \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation 
   323   @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. 
   321   \<open>command_spec\<close> in section~\ref{sec:newcommand}, which simplified the code. 
   324 
   322 
   325   \item {\bf Piotr Trojanek} proofread the text.
   323   \item {\bf Piotr Trojanek} proofread the text.
   326   \end{itemize}
   324   \end{itemize}
   327 
   325 
   328   Please let me know of any omissions. Responsibility for any remaining
   326   Please let me know of any omissions. Responsibility for any remaining
   340 
   338 
   341   \vfill
   339   \vfill
   342   %%This document (version \input{tip.tex}\hspace{-0.5ex}) was compiled with:\\
   340   %%This document (version \input{tip.tex}\hspace{-0.5ex}) was compiled with:\\
   343   %%\input{version.tex}\\
   341   %%\input{version.tex}\\
   344   %% \input{pversion}
   342   %% \input{pversion}
   345 *}
   343 \<close>
   346 
   344 
   347 end
   345 end