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 123 460bc2ee14e9
parent 122 79696161ae16
child 124 0b9fa606a746
equal deleted inserted replaced
122:79696161ae16 123:460bc2ee14e9 
   221   The internal representation of terms uses the usual de Bruijn index mechanism where bound 
   221   The internal representation of terms uses the usual de Bruijn index mechanism where bound 
   222   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
 
   222   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
 
   223   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
 
   223   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
 
   224   binds the corresponding variable. However, in Isabelle the names of bound variables are 
   224   binds the corresponding variable. However, in Isabelle the names of bound variables are 
   225   kept at abstractions for printing purposes, and so should be treated only as comments. 
   225   kept at abstractions for printing purposes, and so should be treated only as comments. 
       
   226   Application in Isabelle is realised with the term-constructor @{ML $}.
 
   226 
   227 
   227   \begin{readmore}
 
   228   \begin{readmore}
 
   228   Terms are described in detail in \isccite{sec:terms}. Their
 
   229   Terms are described in detail in \isccite{sec:terms}. Their
 
   229   definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
 
   230   definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
 
   230   \end{readmore}
 
   231   \end{readmore}
 
   427   result that type-checks.
 
   428   result that type-checks.
 
   428   \end{exercise}
 
   429   \end{exercise}
 
   429 
   430 
   430   (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
 
   431   (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
 
   431 
   432 
       
   433   (FIXME: say something about constants and variables having types as
 
       
   434   arguments and how they can be constructed with fast-type and dummT)
 
   432 *}
 
   435 *}
 
   433 
   436 
   434 section {* Constants *}
 
   437 section {* Constants *}
 
   435 
   438 
   436 text {*
 
   439 text {*
 
   437   There are a few subtle issues with constants. They usually crop up when
 
   440   There are a few subtle issues with constants. They usually crop up when
 
   438   pattern matching terms or constructing term. While it is perfectly ok
 
   441   pattern matching terms or constructing terms. While it is perfectly ok
 
   439   to write the function @{text is_true} as follows
 
   442   to write the function @{text is_true} as follows
 
   440 *}
 
   443 *}
 
   441 
   444 
   442 ML{*fun is_true @{term True} = true
 
   445 ML{*fun is_true @{term True} = true
 
   443   | is_true _ = false*}
 
   446   | is_true _ = false*}
 
   449 
   452 
   450 ML{*fun is_all (@{term All} $ _) = true
 
   453 ML{*fun is_all (@{term All} $ _) = true
 
   451   | is_all _ = false*}
 
   454   | is_all _ = false*}
 
   452 
   455 
   453 text {* 
   456 text {* 
   454   will not correctly match: 
   457   will not correctly match the formula @{prop "\<forall>x::nat. P x"}: 
   455 
   458 
   456   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 
   459   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 
   457 
   460 
   458   The problem is that the @{text "@term"}-antiquotation in the pattern 
   461   The problem is that the @{text "@term"}-antiquotation in the pattern 
   459   fixes the type of @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
   462   fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
   460   an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
   463   an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
   461   for this function is
 
   464   for this function is
 
   462 *}
 
   465 *}
 
   463 
   466 
   464 ML{*fun is_all (Const ("All", _) $ _) = true
 
   467 ML{*fun is_all (Const ("All", _) $ _) = true
 
   467 text {* 
   470 text {* 
   468   because now
 
   471   because now
 
   469 
   472 
   470 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 
   473 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 
   471 
   474 
   472   matches correctly.
 
   475   matches correctly (the wildcard in the pattern matches any type).
 
   473 
   476 
   474   However there is still a problem: consider the function that attempts to 
   477   However there is still a problem: consider the similar function that
 
   475   pick out a @{text "Nil"}-term:
 
   478   attempts to pick out a @{text "Nil"}-term:
 
   476 *}
 
   479 *}
 
   477 
   480 
   478 ML{*fun is_nil (Const ("Nil", _)) = true
 
   481 ML{*fun is_nil (Const ("Nil", _)) = true
 
   479   | is_nil _ = false *}
 
   482   | is_nil _ = false *}
 
   480 
   483 
   481 text {* 
   484 text {* 
   482   Unfortunately, also this one does not return the expected result, since
 
   485   Unfortunately, also this function does \emph{not} work as expected, since
 
   483 
   486 
   484   @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
 
   487   @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
 
   485 
   488 
   486   The problem is that on the ML-level the name of constants is not
 
   489   The problem is that on the ML-level the name of a constant is more
 
   487   immediately clear. If you look at
 
   490   subtle as you might expect. The function @{ML is_all} worked correctly,
 
       
   491   because @{term "All"} is such a fundamental constant, which can be referenced
 
       
   492   by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
 
   488 
   493 
   489   @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 
   494   @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 
   490 
   495 
   491   the name of the constant depends on the theory in which the term constructor
 
   496   the name of the constant depends on the theory in which the term constructor
 
   492   @{text "Nil"} is defined and also in which datatype. Even worse, some
 
   497   @{text "Nil"} is defined (@{text "List"}) and also in which datatype 
   493   constants have an even more complex name involving type-classes. Consider 
   498   (@{text "list"}). Even worse, some constants have a name involving 
   494   for example
 
   499   type-classes. Consider for example the constants for @{term "zero"} 
       
   500   and @{term "(op *)"}:
 
   495 
   501 
   496   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
   502   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
   497   "(Const (\"HOL.zero_class.zero\", \<dots>), 
   503   "(Const (\"HOL.zero_class.zero\", \<dots>), 
   498  Const (\"HOL.times_class.times\", \<dots>))"}
 
   504  Const (\"HOL.times_class.times\", \<dots>))"}
 
   499 
   505 
   500   While you could always use the complete name, for example 
   506   While you could use the complete name, for example 
   501   @{ML "Const (\"List.list.Nil\", @{typ \"nat list\"})"}, for referring to or
 
   507   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
 
   502   matching against @{text "Nil"}, this would make the code rather brittle. 
   508   matching against @{text "Nil"}, this would make the code rather brittle. 
   503   The reason is that the theory and the name of the datatype can easily change. 
   509   The reason is that the theory and the name of the datatype can easily change. 
   504   To make the code more robust it is better to use the antiquotation 
   510   To make the code more robust, it is better to use the antiquotation 
   505   @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
   511   @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
   506   variable parts of the constant's name. Therefore the functions for 
   512   variable parts of the constant's name. Therefore a functions for 
   507   matching against constants should be written as follows.
 
   513   matching against constants that have a polymorphic type should 
       
   514   be written as follows.
 
   508 *}
 
   515 *}
 
   509 
   516 
   510 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
 
   517 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
 
   511   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
 
   518   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
 
   512   | is_nil_or_all _ = false *}
 
   519   | is_nil_or_all _ = false *}
 
   513 
   520 
   514 text {*
 
   521 text {*
 
   515   Having said this, you also frequently have to calculate what the
 
   522   Note that you also frequently have to calculate what the
 
   516   ``base''  name of a constant is. For this you can use the function 
   523   ``base''  name of a given constant is. For this you can use 
   517   @{ML Sign.base_name}. For example:
 
   524   the function @{ML Sign.base_name}. For example:
 
   518   
   525   
   519   (FIXME is there an example for that statement?)
 
   526   (FIXME is there an example for that statement?)
 
   520 
   527 
   521 
   528 
   522   @{ML_response [display,gray] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
 
   529   @{ML_response [display,gray] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
 
   595   \end{readmore}
 
   602   \end{readmore}
 
   596 
   603 
   597   (FIXME: how to add case-names to goal states)
 
   604   (FIXME: how to add case-names to goal states)
 
   598 *}
 
   605 *}
 
   599 
   606 
   600 section {* Theories and Local Theories *}
 
       
   601 
       
   602 section {* Storing Theorems *}
 
       
   603 
       
   604 text {* @{ML PureThy.add_thms_dynamic} *}
 
       
   605 
       
   606 section {* Theorem Attributes *}
 
       
   607 
       
   608 section {* Printing Terms and Theorems\label{sec:printing} *}
 
   607 section {* Printing Terms and Theorems\label{sec:printing} *}
 
   609 
   608 
   610 text {* 
   609 text {* 
   611   During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm} 
   610   During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm} 
   612   or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 
   611   or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 
   654   Again the function @{ML commas} helps with printing more than one theorem. 
   653   Again the function @{ML commas} helps with printing more than one theorem. 
   655 *}
 
   654 *}
 
   656 
   655 
   657 ML{*fun str_of_thms ctxt thms =  
   656 ML{*fun str_of_thms ctxt thms =  
   658   commas (map (str_of_thm ctxt) thms)*}
 
   657   commas (map (str_of_thm ctxt) thms)*}
 
       
   658 
       
   659 section {* Theorem Attributes *}
 
       
   660 
       
   661 section {* Theories and Local Theories *}
 
       
   662 
       
   663 section {* Storing Theorems *}
 
       
   664 
       
   665 text {* @{ML PureThy.add_thms_dynamic} *}
 
   659 
   666 
   660 
   667 
   661 section {* Combinators\label{sec:combinators} *}
 
   668 section {* Combinators\label{sec:combinators} *}
 
   662 
   669 
   663 text {*
 
   670 text {*
isabelle-cookbook