ProgTutorial/FirstSteps.thy
changeset 323 92f6a772e013
parent 322 2b7c08d90e2e
child 324 4172c0743cf2
equal deleted inserted replaced
322:2b7c08d90e2e 323:92f6a772e013
     4 begin
     4 begin
     5 
     5 
     6 chapter {* First Steps *}
     6 chapter {* First Steps *}
     7 
     7 
     8 text {*
     8 text {*
       
     9    \begin{flushright}
       
    10   {\em
       
    11   ``We will most likely never realize the full importance of painting the Tower,\\ 
       
    12   that it is the essential element in the conservation of metal works and the\\ 
       
    13   more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex]
       
    14   Gustave Eiffel, In The 300-Meter Tower.\footnote{The Eiffel Tower has been 
       
    15   re-painted 18 times since its initial construction, an average of once every 
       
    16   seven years. It takes more than a year for a team of 25 painters to paint the Tower 
       
    17   from top to bottom.}\\[1ex]
       
    18   \end{flushright}
       
    19 
     9   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
    20   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
    10   Isabelle must be part of a theory. If you want to follow the code given in
    21   Isabelle must be part of a theory. If you want to follow the code given in
    11   this chapter, we assume you are working inside the theory starting with
    22   this chapter, we assume you are working inside the theory starting with
    12 
    23 
    13   \begin{quote}
    24   \begin{quote}
   670 
   681 
   671   (FIXME: say something about calling conventions) 
   682   (FIXME: say something about calling conventions) 
   672 *}
   683 *}
   673 
   684 
   674 
   685 
   675 section {* Antiquotations *}
   686 section {* ML-Antiquotations *}
   676 
   687 
   677 text {*
   688 text {*
   678   The main advantage of embedding all code in a theory is that the code can
   689   The main advantage of embedding all code in a theory is that the code can
   679   contain references to entities defined on the logical level of Isabelle. By
   690   contain references to entities defined on the logical level of Isabelle. By
   680   this we mean definitions, theorems, terms and so on. This kind of reference is
   691   this we mean definitions, theorems, terms and so on. This kind of reference
   681   realised with antiquotations, sometimes also referred to as ML-antiquotations.  
   692   is realised with ML-antiquotations, often also referred to as just
       
   693   antiquotations.\footnote{There are two kinds of antiquotations in Isabelle,
       
   694   which have very different purpose and infrastructures. The first kind,
       
   695   described in this section, are \emph{ML-antiquotations}. They are used to
       
   696   refer to entities (like terms, types etc) from Isabelle's logic layer inside
       
   697   ML-code. The other kind of antiquotations are \emph{document} antiquotations. They
       
   698   are used only in the text parts of Isabelle and their purpose is to print
       
   699   logical entities inside \LaTeX-documents. They are part of the user level
       
   700   and therefore we are not interested in them in this Tutorial, except in
       
   701   Appendix \ref{rec:docantiquotations} where we show how to implement your own
       
   702   document antiquotations.}
   682   For example, one can print out the name of the current
   703   For example, one can print out the name of the current
   683   theory by typing
   704   theory by typing
   684 
   705 
   685   
   706   
   686   @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
   707   @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
   780   give a pointer to \isacommand{local\_setup}; if not, then explain
   801   give a pointer to \isacommand{local\_setup}; if not, then explain
   781   why @{ML snd} is needed)
   802   why @{ML snd} is needed)
   782 
   803 
   783   It is also possible to define your own antiquotations. But you should
   804   It is also possible to define your own antiquotations. But you should
   784   exercise care when introducing new ones, as they can also make your code
   805   exercise care when introducing new ones, as they can also make your code
   785   also difficult to read. In the next section we will see how the (build in)
   806   also difficult to read. In the next chapter we will see how the (build in)
   786   antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
   807   antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
   787   restriction of this antiquotation is that it does not allow you to use
   808   restriction of this antiquotation is that it does not allow you to use
   788   schematic variables. If you want to have an antiquotation that does not have
   809   schematic variables. If you want to have an antiquotation that does not have
   789   this restriction, you can implement your own using the function @{ML_ind 
   810   this restriction, you can implement your own using the function @{ML_ind
   790   ML_Antiquote.inline}. The code is as follows.
   811   ML_Antiquote.inline}. The code for the antiquotation @{text "term_pat"} is
       
   812   as follows.
   791 *}
   813 *}
   792 
   814 
   793 ML %linenosgray{*ML_Antiquote.inline "term_pat"
   815 ML %linenosgray{*ML_Antiquote.inline "term_pat"
   794   (Args.context -- Scan.lift Args.name_source >>
   816   (Args.context -- Scan.lift Args.name_source >>
   795      (fn (ctxt, s) =>
   817      (fn (ctxt, s) =>
   799 
   821 
   800 text {*
   822 text {*
   801   The parser in Line 2 provides us with a context and a string; this string is
   823   The parser in Line 2 provides us with a context and a string; this string is
   802   transformed into a term using the function @{ML_ind  read_term_pattern in
   824   transformed into a term using the function @{ML_ind  read_term_pattern in
   803   ProofContext} (Line 4); the next two lines print the term so that the
   825   ProofContext} (Line 4); the next two lines print the term so that the
   804   ML-system can understand them. An example of this antiquotation is as
   826   ML-system can understand them. The function @{ML atomic in ML_Syntax}
   805   follows.
   827   just encloses the term in parentheses. An example for the usage of this 
       
   828   antiquotation is:
   806 
   829 
   807   @{ML_response_fake [display,gray]
   830   @{ML_response_fake [display,gray]
   808   "@{term_pat \"Suc (?x::nat)\"}"
   831   "@{term_pat \"Suc (?x::nat)\"}"
   809   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
   832   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
   810 
   833 
   811   which is the internal representation of the term @{text "Suc ?x"}.
   834   which shows the internal representation of the term @{text "Suc ?x"}.
   812 
   835 
   813   \begin{readmore}
   836   \begin{readmore}
   814   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
   837   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
   815   for most antiquotations. 
   838   for most antiquotations. Most of the basic operations on ML-syntax are implemented 
       
   839   in @{ML_file "Pure/ML/ml_syntax.ML"}.
   816   \end{readmore}
   840   \end{readmore}
   817 
   841 *}
   818   Note one source of possible confusion about antiquotations. There are two kinds 
   842 
   819   of them in Isabelle, which have very different purpose and infrastructures. The 
   843 section {* Storing Data (TBD) *}
   820   first kind, described in this section, are \emph{ML-antiquotations}. They are 
   844 
   821   used to refer to entities (like terms, types etc) from Isabelle's logic layer 
   845 text {*
   822   inside ML-code. They are ``linked'' statically at compile-time, which  limits 
   846   Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we 
   823   sometimes their usefulness in  cases where, for example, terms needs to be 
   847   explain this mechanism. 
   824   built up dynamically.  
   848 *}
   825 
   849 
   826   The other kind of antiquotations are \emph{document} antiquotations. 
   850 ML{*signature UNIVERSAL_TYPE =
   827   They are used only in the text parts of Isabelle and their purpose is to print 
   851 sig
   828   logical entities inside \LaTeX-documents. They are part of the user level and
   852   type t
   829   therefore we are not interested in them in this Tutorial, except in 
   853 
   830   Appendix \ref{rec:docantiquotations} where we show how to implement your 
   854   val embed: unit -> ('a -> t) * (t -> 'a option)
   831   own document antiquotations. 
   855 end*}
   832 *}
   856 
       
   857 ML{*structure U:> UNIVERSAL_TYPE =
       
   858    struct
       
   859       type t = exn
       
   860 
       
   861       fun 'a embed () =
       
   862          let
       
   863             exception E of 'a
       
   864             fun project (e: t): 'a option =
       
   865                case e of
       
   866                   E a => SOME a
       
   867                 | _ => NONE
       
   868          in
       
   869             (E, project)
       
   870          end
       
   871    end*}
       
   872 
       
   873 text {*
       
   874   The idea is that type t is the universal type and that each call to embed
       
   875   returns a new pair of functions (inject, project), where inject embeds a
       
   876   value into the universal type and project extracts the value from the
       
   877   universal type. A pair (inject, project) returned by embed works together in
       
   878   that project u will return SOME v if and only if u was created by inject
       
   879   v. If u was created by a different function inject', then project returns
       
   880   NONE.
       
   881 
       
   882   in library.ML
       
   883 *}
       
   884 
       
   885 ML_val{*structure Object = struct type T = exn end; *}
       
   886 
       
   887 ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
       
   888    struct
       
   889       val (intIn: int -> U.t, intOut) = U.embed ()
       
   890       val r: U.t ref = ref (intIn 13)
       
   891       val s1 =
       
   892          case intOut (!r) of
       
   893             NONE => "NONE"
       
   894           | SOME i => Int.toString i
       
   895       val (realIn: real -> U.t, realOut) = U.embed ()
       
   896       val _ = r := realIn 13.0
       
   897       val s2 =
       
   898          case intOut (!r) of
       
   899             NONE => "NONE"
       
   900           | SOME i => Int.toString i
       
   901       val s3 =
       
   902          case realOut (!r) of
       
   903             NONE => "NONE"
       
   904           | SOME x => Real.toString x
       
   905       val _ = tracing (implode [s1, " ", s2, " ", s3, "\n"])
       
   906    end*}
       
   907 
       
   908 ML_val{*structure t = Test(U) *} 
       
   909 
       
   910 ML_val{*structure Datatab = Table(type key = int val ord = int_ord);*}
       
   911 
       
   912 ML {* LocalTheory.restore *}
       
   913 ML {* LocalTheory.set_group *}
       
   914 
       
   915 
   833 
   916 
   834 (*
   917 (*
   835 section {* Do Not Try This At Home! *}
   918 section {* Do Not Try This At Home! *}
   836 
   919 
   837 ML {* val my_thms = ref ([]: thm list) *}
   920 ML {* val my_thms = ref ([]: thm list) *}