Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CookBook/FirstSteps.thy
changeset 19 34b93dbf8c3c
parent 15 9da9ba2b095b
child 20 5ae6a1bb91c9
equal deleted inserted replaced
18:b4c31af6af26 19:34b93dbf8c3c 
    34 ML {*
 
    34 ML {*
 
    35   3 + 4
 
    35   3 + 4
 
    36 *}
 
    36 *}
 
    37 
    37 
    38 text {*
 
    38 text {*
 
    39   The expression inside \isacommand{ML} commands is immediately evaluated,
 
    39   Expressions inside \isacommand{ML} commands are immediately evaluated,
 
    40   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
    40   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
    41   your Isabelle environment. The code inside the \isacommand{ML} command 
    41   your Isabelle environment. The code inside the \isacommand{ML} command 
    42   can also contain value and function bindings. However on such \isacommand{ML}
 
    42   can also contain value and function bindings. However on such \isacommand{ML}
 
    43   commands the undo operation behaves slightly counter-intuitive, because 
    43   commands the undo operation behaves slightly counter-intuitive, because 
    44   if you define
 
    44   if you define
 
    78 
    78 
    79 ML {* warning "any string" *}
 
    79 ML {* warning "any string" *}
 
    80 
    80 
    81 text {*
 
    81 text {*
 
    82   will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
 
    82   will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
 
    83   PolyML provides a convenient, though again ``quick-and-dirty'', method for 
    83   If you develop under PolyML, then there is a convenient, though again 
    84   converting arbitrary values into strings, for example: 
    84   ``quick-and-dirty'', method for converting values into strings, 
       
    85   for example: 
    85 *}
 
    86 *}
 
    86 
    87 
    87 ML {* warning (makestring 1) *}
 
    88 ML {* warning (makestring 1) *}
 
    88 
    89 
    89 text {*
 
    90 text {*
 
    90   However this only works if the type of what is printed is monomorphic and not 
    91   However this only works if the type of what is converted is monomorphic and not 
    91   a function.
 
    92   a function.
 
    92 *}
 
    93 *}
 
    93 
    94 
    94 text {* 
    95 text {* 
    95   The funtion warning should only be used for testing purposes, because
 
    96   The funtion warning should only be used for testing purposes, because
 
    96   any output this funtion generated will be overwritten, if an error is raised. 
    97   any output this funtion generates will be overwritten, as soon as an error 
    97   For printing anything more serious and elaborate, the function @{ML tracing}
 
    98   is raised. 
    98   should be used. This function writes all output in a separate buffer.
 
    99   Therefore for printing anything more serious and elaborate, the function @{ML tracing}
 
       
   100   should be used. This function writes all output into a separate buffer.
 
    99 *}
 
   101 *}
 
   100 
   102 
   101 ML {* tracing "foo" *}
 
   103 ML {* tracing "foo" *}
 
   102 
   104 
   103 text {* 
   105 text {* 
   122      TextIO.output (stream, "\n");
 
   124      TextIO.output (stream, "\n");
 
   123      TextIO.flushOut stream));
 
   125      TextIO.flushOut stream));
 
   124 *}
 
   126 *}
 
   125 
   127 
   126 text {* 
   128 text {* 
   127   Calling the @{ML_text "redirect_tracing"} function with @{ML_text "(TextIO.openOut \"foo.bar\")"} 
   129   Calling @{ML_text "redirect_tracing"} with @{ML_text "(TextIO.openOut \"foo.bar\")"} 
   128   will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
 
   130   will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
 
   129 
   131 
   130 *}
 
   132 *}
 
   131 
   133 
   132 
   134 
   152   determined at ``compile-time'', not ``run-time''. For example the function
 
   154   determined at ``compile-time'', not ``run-time''. For example the function
 
   153 
   155 
   154 *}
 
   156 *}
 
   155 
   157 
   156 ML {* 
   158 ML {* 
   157   fun current_thyname () = Context.theory_name @{theory}
 
   159   fun not_current_thyname () = Context.theory_name @{theory}
 
   158 *}
 
   160 *}
 
   159 
   161 
   160 text {*
 
   162 text {*
 
   161   does \emph{not} return the name of the current theory, if it is run in a 
   163   does \emph{not} return the name of the current theory, if it is run in a 
   162   different theory. Instead, the code above defines the constant function 
   164   different theory. Instead, the code above defines the constant function 
   164   function is called. Operationally speaking,  @{text "@{theory}"} is 
   166   function is called. Operationally speaking,  @{text "@{theory}"} is 
   165   \emph{not} replaced with code that will look up the current theory in 
   167   \emph{not} replaced with code that will look up the current theory in 
   166   some data structure and return it. Instead, it is literally
 
   168   some data structure and return it. Instead, it is literally
 
   167   replaced with the value representing the theory name.
 
   169   replaced with the value representing the theory name.
 
   168 
   170 
   169   In a similar way you can use antiquotations to refer to types and theorems:
 
   171   In a similar way you can use antiquotations to refer to theorems:
 
   170 *}
 
   172 *}
 
   171 
   173 
   172 ML {* @{typ "(int * nat) list"} *}
 
       
   173 ML {* @{thm allI} *}
 
   174 ML {* @{thm allI} *}
 
   174 
   175 
   175 text {*
 
   176 text {*
 
   176   In the course of this introduction, we will learn more about 
   177   In the course of this introduction, we will learn more about 
   177   these antiquotations: they greatly simplify Isabelle programming since one
 
   178   these antiquotations: they greatly simplify Isabelle programming since one
 
   236 
   237 
   237 *}
 
   238 *}
 
   238 
   239 
   239 ML {* @{term "P x"} ; @{prop "P x"} *}
 
   240 ML {* @{term "P x"} ; @{prop "P x"} *}
 
   240 
   241 
   241 text {* which inserts the coercion in the latter ase and *}
 
   242 text {* which inserts the coercion in the latter case and *}
 
   242 
   243 
   243 
   244 
   244 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
   245 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
   245 
   246 
   246 text {* which does not. *}
 
   247 text {* 
   247 
   248   which does not. 
   248 text {* (FIXME: add something about @{text "@{typ \<dots>}"}) *}
 
   249 
       
   250   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
 
       
   251   
       
   252   *}
 
       
   253 
       
   254 ML {* @{typ "bool \<Rightarrow> nat"} *}
 
       
   255 
       
   256 text {*
 
       
   257   (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the
 
       
   258   internal representation. Is there a reason for this, that needs to be explained 
       
   259   here?)
 
       
   260 
       
   261   \begin{readmore}
 
       
   262   Types are described in detail in \isccite{sec:types}. Their
 
       
   263   definition and many useful operations can be found in @{ML_file "Pure/type.ML"}.
 
       
   264   \end{readmore}
 
       
   265 
       
   266   *}
 
       
   267 
       
   268 
       
   269 
   249 
   270 
   250 section {* Constructing Terms and Types Manually *} 
   271 section {* Constructing Terms and Types Manually *} 
   251 
   272 
   252 text {*
 
   273 text {*
 
   253 
   274 
   254   While antiquotations are very convenient for constructing terms (similarly types), 
   275   While antiquotations are very convenient for constructing terms and types, 
   255   they can only construct fixed terms. Unfortunately, one often needs to construct them 
   276   they can only construct fixed terms. Unfortunately, one often needs to construct them 
   256   dynamically. For example, a function that returns the implication 
   277   dynamically. For example, a function that returns the implication 
   257   @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments
 
   278   @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
 
   258   can only be written as
 
   279   as arguments can only be written as
 
   259 *}
 
   280 *}
 
   260 
   281 
   261 
   282 
   262 ML {*
 
   283 ML {*
 
   263   fun make_imp P Q =
 
   284   fun make_imp P Q tau =
 
   264   let
 
   285   let
 
   265     val x = @{term "x::nat"}
 
   286     val x = Free ("x",tau)
 
   266   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
 
   287   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
 
   267                                     HOLogic.mk_Trueprop (Q $ x)))
 
   288                                     HOLogic.mk_Trueprop (Q $ x)))
 
   268   end
 
   289   end
 
   269 *}
 
   290 *}
 
   270 
   291 
   271 text {*
 
   292 text {*
 
   272 
   293 
   273   The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
   294   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
   274   an antiquotation. For example this following does not work.
 
   295   @{term "tau"} into an antiquotation. For example this following does not work.
 
   275 *}
 
   296 *}
 
   276 
   297 
   277 ML {*
 
   298 ML {*
 
   278   fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
   299   fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
   279 *}
 
   300 *}
 
   280 
   301 
   281 text {*
 
   302 text {*
 
   282 
   303 
   283   To see this apply @{text "@{term S}"} and @{text "@{term T}"} to boths functions.
 
   304   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
   284   
   305   to both functions. 
   285   One tricky point in constructing terms by hand is to obtain the fully qualified 
   306 
   286   name for constants. For example the names for @{text "zero"} or @{text "+"} are
 
   307   One tricky point in constructing terms by hand is to obtain the 
   287   more complex than one first expects, namely 
   308   fully qualified name for constants. For example the names for @{text "zero"} or 
       
   309   @{text "+"} are more complex than one first expects, namely 
   288 
   310 
   289   \begin{center}
 
   311   \begin{center}
 
   290   @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. 
   312   @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. 
   291   \end{center}
 
   313   \end{center}
 
   292   
   314   
   293   The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because 
   315   The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because 
   294   these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
   316   these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
   295   which theory they are defined. Guessing such internal names can sometimes be quite hard. 
   317   which theory they are defined. Guessing such internal names can sometimes be quite hard. 
   296   Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
   318   Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
   297   expansion automatically, for example:
 
   319   expansion automatically, for example:
 
   298 
   320 *}
 
   299 *}
 
   321  
   300 
   322 text {*
 
   301 ML {* @{const_name HOL.zero}; @{const_name  plus} *}
 
   323 
   302 
   324   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 
   303 text {*
 
       
   304 
   325 
   305   \begin{readmore}
 
   326   \begin{readmore}
 
   306   There are many functions in @{ML_file "Pure/logic.ML"} and
 
   327   There are many functions in @{ML_file "Pure/logic.ML"} and
 
   307   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
   328   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
   308   easier.\end{readmore}
 
   329   easier.\end{readmore}
isabelle-cookbook