ProgTutorial/First_Steps.thy
changeset 557 77ea2de0ca62
parent 554 638ed040e6f8
child 559 ffa5c4ec9611
equal deleted inserted replaced
556:3c214b215f7e 557:77ea2de0ca62
     1 theory First_Steps
     1 theory First_Steps
     2 imports Base
     2 imports Base
     3 begin
     3 begin
     4 
     4                                                   
     5 
       
     6 chapter {* First Steps\label{chp:firststeps} *}
     5 chapter {* First Steps\label{chp:firststeps} *}
     7 
     6 
     8 text {*
     7 text {*
     9   \begin{flushright}
     8   \begin{flushright}
    10   {\em ``The most effective debugging tool is still careful thought,\\ 
     9   {\em ``The most effective debugging tool is still careful thought,\\ 
    96   code. This can be done in a ``quick-and-dirty'' fashion using the function
    95   code. This can be done in a ``quick-and-dirty'' fashion using the function
    97   @{ML_ind writeln in Output}. For example
    96   @{ML_ind writeln in Output}. For example
    98 
    97 
    99   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
    98   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
   100 
    99 
   101   will print out @{text [quotes] "any string"} inside the response buffer.  
   100   will print out @{text [quotes] "any string"}.  
   102   This function expects a string as argument. If you develop under
   101   This function expects a string as argument. If you develop under
   103   PolyML, then there is a convenient, though again ``quick-and-dirty'', method
   102   PolyML, then there is a convenient, though again ``quick-and-dirty'', method
   104   for converting values into strings, namely the antiquotation 
   103   for converting values into strings, namely the antiquotation 
   105   @{text "@{make_string}"}:
   104   @{text "@{make_string}"}:
   106 
   105 
   112   You can print out error messages with the function @{ML_ind error in Library}; 
   111   You can print out error messages with the function @{ML_ind error in Library}; 
   113   for example:
   112   for example:
   114 
   113 
   115   @{ML_response_fake [display,gray] 
   114   @{ML_response_fake [display,gray] 
   116   "if 0 = 1 then true else (error \"foo\")" 
   115   "if 0 = 1 then true else (error \"foo\")" 
   117 "Exception- ERROR \"foo\" raised
   116 "*** foo
   118 At command \"ML\"."}
   117 ***"}
   119 
   118 
   120   This function raises the exception @{text ERROR}, which will then 
   119   This function raises the exception @{text ERROR}, which will then 
   121   be displayed by the infrastructure. Note that this exception is meant 
   120   be displayed by the infrastructure indicating that it is an error by
       
   121   painting the output red. Note that this exception is meant 
   122   for ``user-level'' error messages seen by the ``end-user''. 
   122   for ``user-level'' error messages seen by the ``end-user''. 
   123   For messages where you want to indicate a genuine program error, then
   123   For messages where you want to indicate a genuine program error, then
   124   use the exception @{text Fail}. 
   124   use the exception @{text Fail}. 
   125 
   125 
   126   Most often you want to inspect data of Isabelle's basic data structures,
   126   Most often you want to inspect data of Isabelle's basic data structures,
   150 ML %grayML{*fun pretty_terms ctxt trms =  
   150 ML %grayML{*fun pretty_terms ctxt trms =  
   151   Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
   151   Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
   152 
   152 
   153 text {*
   153 text {*
   154   You can also print out terms together with their typing information.
   154   You can also print out terms together with their typing information.
   155   For this you need to set the configuration value 
   155   For this you need to set the configuration value  
   156   @{ML_ind show_types in Syntax} to @{ML true}.
   156   @{ML_ind show_types in Syntax} to @{ML true}.
   157 *}
   157 *}
   158 
   158 
   159 ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*}
   159 ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*}
   160 
   160 
   541   where the return value of the recursive call is bound explicitly to
   541   where the return value of the recursive call is bound explicitly to
   542   the pair @{ML "(los, grs)" for los grs}. However, this function
   542   the pair @{ML "(los, grs)" for los grs}. However, this function
   543   can be implemented more concisely as
   543   can be implemented more concisely as
   544 *}
   544 *}
   545 
   545 
   546 ML %grayML{*fun separate i [] = ([], [])
   546 ML %grayML{*fun separate _ [] = ([], [])
   547   | separate i (x::xs) =
   547   | separate i (x::xs) =
   548       if i <= x 
   548       if i <= x 
   549       then separate i xs ||> cons x
   549       then separate i xs ||> cons x
   550       else separate i xs |>> cons x*}
   550       else separate i xs |>> cons x*}
   551 
   551 
   770 
   770 
   771   Another important antiquotation is @{text "@{context}"}. (What the
   771   Another important antiquotation is @{text "@{context}"}. (What the
   772   difference between a theory and a context is will be described in Chapter
   772   difference between a theory and a context is will be described in Chapter
   773   \ref{chp:advanced}.) A context is for example needed in order to use the
   773   \ref{chp:advanced}.) A context is for example needed in order to use the
   774   function @{ML print_abbrevs in Proof_Context} that list of all currently
   774   function @{ML print_abbrevs in Proof_Context} that list of all currently
   775   defined abbreviations.
   775   defined abbreviations. For example
   776 
   776 
   777   @{ML_response_fake [display, gray]
   777   @{ML_response_fake [display, gray]
   778   "Proof_Context.print_abbrevs @{context}"
   778   "Proof_Context.print_abbrevs @{context}"
   779 "Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
   779 "\<dots>
   780 INTER \<equiv> INFI
   780 INTER \<equiv> INFI
   781 Inter \<equiv> Inf
   781 Inter \<equiv> Inf
   782 \<dots>"}
   782 \<dots>"}
   783 
   783 
       
   784   The precise output of course depends on the abbreviations that are
       
   785   currently defined; this can change over time.
   784   You can also use antiquotations to refer to proved theorems: 
   786   You can also use antiquotations to refer to proved theorems: 
   785   @{text "@{thm \<dots>}"} for a single theorem
   787   @{text "@{thm \<dots>}"} for a single theorem
   786 
   788 
   787   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
   789   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
   788 
   790 
   810   It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
   812   It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
   811   whose first argument is a statement (possibly many of them separated by @{text "and"})
   813   whose first argument is a statement (possibly many of them separated by @{text "and"})
   812   and the second is a proof. For example
   814   and the second is a proof. For example
   813 *}
   815 *}
   814 
   816 
   815 ML %grayML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
   817 ML %grayML{*val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
   816 
   818 
   817 text {*
   819 text {*
   818   The result can be printed out as follows.
   820   The result can be printed out as follows.
   819 
   821 
   820   @{ML_response_fake [gray,display]
   822   @{ML_response_fake [gray,display]
   821 "foo_thm |> pretty_thms_no_vars @{context}
   823 "foo_thms |> pretty_thms_no_vars @{context}
   822         |> pwriteln"
   824          |> pwriteln"
   823   "True, False \<Longrightarrow> P"}
   825   "True, False \<Longrightarrow> P"}
   824 
   826 
   825   You can also refer to the current simpset via an antiquotation. To illustrate 
   827   You can also refer to the current simpset via an antiquotation. To illustrate 
   826   this we implement the function that extracts the theorem names stored in a 
   828   this we implement the function that extracts the theorem names stored in a 
   827   simpset.
   829   simpset.
   913   which can be installed with
   915   which can be installed with
   914 *}
   916 *}
   915 
   917 
   916 setup %gray {* type_pat_setup *}
   918 setup %gray {* type_pat_setup *}
   917 
   919 
   918 text {*
   920 text {* 
   919   However, a word of warning is in order: Introducing new antiquotations
   921 However, a word of warning is in order: Introducing new antiquotations should be done only after
   920   should be done only after careful deliberations. They can make your 
   922 careful deliberations. They can potentially make your code harder to read, than making it easier.
   921   code harder to read, than making it easier. 
       
   922 
   923 
   923   \begin{readmore}
   924   \begin{readmore}
   924   The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
   925   The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
   925   contain the infrastructure and definitions for most antiquotations. Most of the basic operations 
   926   contain the infrastructure and definitions for most antiquotations. Most of the basic operations 
   926   on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
   927   on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
   990 true"}
   991 true"}
   991 
   992 
   992   Notice that we access the integer as an integer and the boolean as
   993   Notice that we access the integer as an integer and the boolean as
   993   a boolean. If we attempt to access the integer as a boolean, then we get 
   994   a boolean. If we attempt to access the integer as a boolean, then we get 
   994   a runtime error. 
   995   a runtime error. 
   995   
   996 
   996   @{ML_response_fake [display, gray]
   997   @{ML_response_fake [display, gray]
   997 "project_bool (nth foo_list 0)"  
   998 "project_bool (nth foo_list 0)"  
   998 "*** Exception- Match raised"}
   999 "*** exception Match raised"}
   999 
  1000 
  1000   This runtime error is the reason why ML is still type-sound despite
  1001   This runtime error is the reason why ML is still type-sound despite
  1001   containing a universal type.
  1002   containing a universal type.
  1002 
  1003 
  1003   Now, Isabelle heavily uses this mechanism for storing all sorts of
  1004   Now, Isabelle heavily uses this mechanism for storing all sorts of
  1214 
  1215 
  1215   For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, 
  1216   For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, 
  1216   for treating theories and proof contexts more uniformly. This type is defined as follows
  1217   for treating theories and proof contexts more uniformly. This type is defined as follows
  1217 *}
  1218 *}
  1218 
  1219 
  1219 ML_val{*datatype generic = 
  1220 ML_val %grayML{*datatype generic = 
  1220   Theory of theory 
  1221   Theory of theory 
  1221 | Proof of proof*}
  1222 | Proof of proof*}
  1222 
  1223 
  1223 text {*
  1224 text {*
  1224   \footnote{\bf FIXME: say more about generic contexts.}
  1225   \footnote{\bf FIXME: say more about generic contexts.}