diff -r 26e5b41faa74 -r 79696161ae16 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Feb 16 17:17:24 2009 +0000 +++ b/CookBook/FirstSteps.thy Tue Feb 17 02:12:19 2009 +0000 @@ -114,7 +114,9 @@ You can print out error messages with the function @{ML error}; for example: - @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""} +@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" +"Exception- ERROR \"foo\" raised +At command \"ML\"."} Section~\ref{sec:printing} will give more information about printing the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} @@ -122,8 +124,6 @@ *} - - section {* Antiquotations *} text {* @@ -161,7 +161,7 @@ @{ML_response_fake [display,gray] "@{thm allI}" "(\x. ?P x) \ \x. ?P x"} - and simpsets: + and current simpsets: @{ML_response_fake [display,gray] "let @@ -171,7 +171,7 @@ end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} The code about simpsets extracts the theorem names stored in the - current simpset. You can get hold of the current simpset with the antiquotation + simpset. You can get hold of the current simpset with the antiquotation @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record containing all information about the simpset. The rules of a simpset are stored in a \emph{discrimination net} (a data structure for fast @@ -197,8 +197,8 @@ packages. Antiquotations solve this problem, since they are ``linked'' statically at compile-time. However, this static linkage also limits their usefulness in cases where data needs to be build up dynamically. In the - course of this introduction, we will learn more about these antiquotations: - they greatly simplify Isabelle programming since one can directly access all + course of this introduction, you will learn more about these antiquotations: + they can simplify Isabelle programming since one can directly access all kinds of logical elements from th ML-level. *} @@ -206,7 +206,7 @@ section {* Terms and Types *} text {* - One way to construct terms of Isabelle on the ML-level is by using the antiquotation + One way to construct terms of Isabelle is by using the antiquotation \mbox{@{text "@{term \}"}}. For example: @{ML_response [display,gray] @@ -245,8 +245,8 @@ Hint: The third term is already quite big, and the pretty printer may omit parts of it by default. If you want to see all of it, you - can use the following ML-function to set the limit to a value high - enough: + can use the following ML-function to set the printing depth to a higher + value: @{ML [display,gray] "print_depth 50"} \end{exercise} @@ -323,28 +323,6 @@ Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ (Const \ $ (Free (\"Q\",\) $ \)))"} - (FIXME: expand the following point) - - One tricky point in constructing terms by hand is to obtain the fully - qualified name for constants. For example the names for @{text "zero"} and - @{text "+"} are more complex than one first expects, namely - - - \begin{center} - @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. - \end{center} - - The extra prefixes @{text zero_class} and @{text plus_class} are present - because these constants are defined within type classes; the prefix @{text - "HOL"} indicates in which theory they are defined. Guessing such internal - names can sometimes be quite hard. Therefore Isabelle provides the - antiquotation @{text "@{const_name \}"} which does the expansion - automatically, for example: - - @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"} - - (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) - Although types of terms can often be inferred, there are many situations where you need to construct types manually, especially when defining constants. For example the function returning a function @@ -359,21 +337,19 @@ ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *} text {* - \begin{readmore} There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms and types easier.\end{readmore} Have a look at these files and try to solve the following two exercises: - *} text {* \begin{exercise}\label{fun:revsum} Write a function @{text "rev_sum : term -> term"} that takes a - term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} (whereby @{text "i"} might be zero) + term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} (whereby @{text "n"} might be zero) and returns the reversed sum @{text "t\<^isub>n + \ + t\<^isub>2 + t\<^isub>1"}. Assume the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} associates to the left. Try your function on some examples. @@ -387,7 +363,7 @@ A handy function for manipulating terms is @{ML map_types}: it takes a function and applies it to every type in the term. You can, for example, - change every @{typ nat} in a term into an @{typ int} using the function + change every @{typ nat} in a term into an @{typ int} using the function: *} ML{*fun nat_to_int t = @@ -397,8 +373,7 @@ | _ => t)*} text {* - an then apply it as follows: - + An example as follows: @{ML_response_fake [display,gray] "map_types nat_to_int @{term \"a = (1::nat)\"}" @@ -456,11 +431,109 @@ *} +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 + to write the function @{text is_true} as follows +*} + +ML{*fun is_true @{term True} = true + | is_true _ = false*} + +text {* + this does not work for picking out @{text "\"}-quantified terms. Because + the function +*} + +ML{*fun is_all (@{term All} $ _) = true + | is_all _ = false*} + +text {* + will not correctly match: + + @{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 + an arbitrary, but fixed type @{typ "'a"}. A properly working alternative + for this function is +*} + +ML{*fun is_all (Const ("All", _) $ _) = true + | is_all _ = false*} + +text {* + because now + +@{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "true"} + + matches correctly. + + However there is still a problem: consider the 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 + + @{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 + + @{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 + + @{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 + 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 + @{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. +*} + +ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true + | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true + | 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: + + (FIXME is there an example for that statement?) + + + @{ML_response [display,gray] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} + + (FIXME authentic syntax?) + + \begin{readmore} + FIXME + \end{readmore} +*} + + section {* Theorems *} text {* Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} - that can only be built by going through interfaces. As a consequence, every proof + that can only be build by going through interfaces. As a consequence, every proof in Isabelle is correct by construction. (FIXME reference LCF-philosophy) @@ -585,30 +658,6 @@ commas (map (str_of_thm ctxt) thms)*} -section {* Operations on Constants (Names) *} - -text {* - -@{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} - - authentic syntax? - -*} - -ML {* @{const_name lfp} *} - -text {* - constants in case-patterns? - - In the meantime, lfp has been moved to the Inductive theory, so it is - no longer called Lfp.lfp. If a @{text "@{const_name}"} antiquotation had been - used, we would have gotten an error for this. Another advantage of the - antiquotation is that we can then just write @{text "@{const_name lfp}"} rather - than @{text "@{const_name Lfp.lfp}"} or whatever, and it expands to the correct - name. - -*} - section {* Combinators\label{sec:combinators} *} text {*