# HG changeset patch # User Christian Urban # Date 1234878834 0 # Node ID 460bc2ee14e916044b4e25b623a91d6d430d5c72 # Parent 79696161ae16066441928f86842b7be29b9a5ba6 some polishing in the first-steps chapter diff -r 79696161ae16 -r 460bc2ee14e9 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Tue Feb 17 02:12:19 2009 +0000 +++ b/CookBook/FirstSteps.thy Tue Feb 17 13:53:54 2009 +0000 @@ -223,6 +223,7 @@ the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that binds the corresponding variable. However, in Isabelle the names of bound variables are kept at abstractions for printing purposes, and so should be treated only as comments. + Application in Isabelle is realised with the term-constructor @{ML $}. \begin{readmore} Terms are described in detail in \isccite{sec:terms}. Their @@ -429,13 +430,15 @@ (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT}) + (FIXME: say something about constants and variables having types as + arguments and how they can be constructed with fast-type and dummT) *} section {* Constants *} text {* There are a few subtle issues with constants. They usually crop up when - pattern matching terms or constructing term. While it is perfectly ok + pattern matching terms or constructing terms. While it is perfectly ok to write the function @{text is_true} as follows *} @@ -451,12 +454,12 @@ | is_all _ = false*} text {* - will not correctly match: + will not correctly match the formula @{prop "\x::nat. P x"}: @{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "false"} The problem is that the @{text "@term"}-antiquotation in the pattern - fixes the type of @{term "All"} to be @{typ "('a \ bool) \ bool"} for + fixes the type of the constant @{term "All"} to be @{typ "('a \ bool) \ bool"} for an arbitrary, but fixed type @{typ "'a"}. A properly working alternative for this function is *} @@ -469,42 +472,46 @@ @{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "true"} - matches correctly. + matches correctly (the wildcard in the pattern matches any type). - However there is still a problem: consider the function that attempts to - pick out a @{text "Nil"}-term: + However there is still a problem: consider the similar function that + attempts to pick out a @{text "Nil"}-term: *} ML{*fun is_nil (Const ("Nil", _)) = true | is_nil _ = false *} text {* - Unfortunately, also this one does not return the expected result, since + Unfortunately, also this function does \emph{not} work as expected, since @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"} - The problem is that on the ML-level the name of constants is not - immediately clear. If you look at + The problem is that on the ML-level the name of a constant is more + subtle as you might expect. The function @{ML is_all} worked correctly, + because @{term "All"} is such a fundamental constant, which can be referenced + by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \)"} the name of the constant depends on the theory in which the term constructor - @{text "Nil"} is defined and also in which datatype. Even worse, some - constants have an even more complex name involving type-classes. Consider - for example + @{text "Nil"} is defined (@{text "List"}) and also in which datatype + (@{text "list"}). Even worse, some constants have a name involving + type-classes. Consider for example the constants for @{term "zero"} + and @{term "(op *)"}: @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" "(Const (\"HOL.zero_class.zero\", \), Const (\"HOL.times_class.times\", \))"} - While you could always use the complete name, for example - @{ML "Const (\"List.list.Nil\", @{typ \"nat list\"})"}, for referring to or + While you could use the complete name, for example + @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or matching against @{text "Nil"}, this would make the code rather brittle. The reason is that the theory and the name of the datatype can easily change. - To make the code more robust it is better to use the antiquotation + To make the code more robust, it is better to use the antiquotation @{text "@{const_name \}"}. With this antiquotation you can harness the - variable parts of the constant's name. Therefore the functions for - matching against constants should be written as follows. + variable parts of the constant's name. Therefore a functions for + matching against constants that have a polymorphic type should + be written as follows. *} ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true @@ -512,9 +519,9 @@ | is_nil_or_all _ = false *} text {* - Having said this, you also frequently have to calculate what the - ``base'' name of a constant is. For this you can use the function - @{ML Sign.base_name}. For example: + Note that you also frequently have to calculate what the + ``base'' name of a given constant is. For this you can use + the function @{ML Sign.base_name}. For example: (FIXME is there an example for that statement?) @@ -597,14 +604,6 @@ (FIXME: how to add case-names to goal states) *} -section {* Theories and Local Theories *} - -section {* Storing Theorems *} - -text {* @{ML PureThy.add_thms_dynamic} *} - -section {* Theorem Attributes *} - section {* Printing Terms and Theorems\label{sec:printing} *} text {* @@ -657,6 +656,14 @@ ML{*fun str_of_thms ctxt thms = commas (map (str_of_thm ctxt) thms)*} +section {* Theorem Attributes *} + +section {* Theories and Local Theories *} + +section {* Storing Theorems *} + +text {* @{ML PureThy.add_thms_dynamic} *} + section {* Combinators\label{sec:combinators} *} diff -r 79696161ae16 -r 460bc2ee14e9 cookbook.pdf Binary file cookbook.pdf has changed