diff -r 84d1392186d3 -r 253ea99c1441 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Feb 25 22:13:41 2009 +0000 +++ b/CookBook/FirstSteps.thy Thu Feb 26 12:16:24 2009 +0000 @@ -141,9 +141,9 @@ Syntax.string_of_term ctxt (term_of t)*} text {* - The function @{ML term_of} extracts the @{ML_type term} from a @{ML_type cterm}. - If there are more than one @{ML_type cterm}s to be printed, you can use the - function @{ML commas} to separate them. + In this example the function @{ML term_of} extracts the @{ML_type term} from + a @{ML_type cterm}. If there are more than one @{ML_type cterm}s to be + printed, you can use the function @{ML commas} to separate them. *} ML{*fun str_of_cterms ctxt ts = @@ -214,7 +214,7 @@ common when dealing with theories (for example by adding a definition, followed by lemmas and so on). The reverse application allows you to read what happens in a top-down manner. This kind of coding should also be familiar, - if you used to Haskell's do-notation. Writing the function @{ML inc_by_five} using + if you have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using the reverse application is much clearer than writing *} @@ -389,11 +389,11 @@ (?P \ ?Q \ ?R) = (?Q \ ?P \ ?R) ((?P \ ?Q) \ ?R) = (?P \ ?Q \ ?R)"} - You can also refer to the current simpset. To illustrate this we use the + You can also refer to the current simpset. To illustrate this we implement the function that extracts the theorem names stored in a simpset. *} -ML{*fun get_thm_names simpset = +ML{*fun get_thm_names_from_ss simpset = let val ({rules,...}, _) = MetaSimplifier.rep_ss simpset in @@ -405,13 +405,13 @@ information about the simpset. The rules of a simpset are stored in a \emph{discrimination net} (a data structure for fast indexing). From this net you can extract the entries using the function @{ML Net.entries}. - You can now use @{ML get_thm_names} to obtain all names of theorems stored + You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored in the current simpset---this simpset can be referred to using the antiquotation - @{text "@{simpset}"}.\footnote - {FIXME: you cannot cleanly match against lists with ommited parts} + @{text "@{simpset}"}. @{ML_response_fake [display,gray] -"get_thm_names @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} + "get_thm_names_from_ss @{simpset}" + "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} \begin{readmore} The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"} @@ -431,7 +431,7 @@ 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, you will learn more about these antiquotations: + course of this chapter 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. @@ -446,7 +446,7 @@ @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" "Const (\"op =\", \) $ - (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} + (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} This will show the term @{term "(a::nat) + b = c"}, but printed using the internal representation of this term. This internal representation corresponds to the @@ -456,7 +456,7 @@ variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to 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. + 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} @@ -492,7 +492,7 @@ @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \) $ Free (\"x\", \), - Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} + Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} where a coercion is inserted in the second component and @@ -617,7 +617,7 @@ \end{exercise} There are a few subtle issues with constants. They usually crop up when - pattern matching terms or types, or constructing them. While it is perfectly ok + pattern matching terms or types, or when constructing them. While it is perfectly ok to write the function @{text is_true} as follows *} @@ -651,7 +651,8 @@ @{ML_response [display,gray] "is_all @{term \"\x::nat. P x\"}" "true"} - matches correctly (the first wildcard in the pattern matches any type). + matches correctly (the first wildcard in the pattern matches any type and the + second any term). However there is still a problem: consider the similar function that attempts to pick out @{text "Nil"}-terms: @@ -666,7 +667,7 @@ @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"} 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, + subtle than 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 @@ -732,7 +733,7 @@ the @{ML "@{theory}"} antiquotation to get hold of the current theory. For example you can write: - @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"} + @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"} This can also be written with an antiquotation: @@ -770,15 +771,15 @@ To calculate the type, this function traverses the whole term and will detect any typing inconsistency. For examle changing the type of the variable - from @{typ "nat"} to @{typ "int"} will result in the error message: + @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: @{ML_response_fake [display,gray] "type_of (@{term \"f::nat \ bool\"} $ @{term \"x::int\"})" "*** Exception- TYPE (\"type_of: type mismatch in application\" \"} Since the complete traversal might sometimes be too costly and - not necessary, there is also the function @{ML fastype_of}, which - returns the type of a term. + not necessary, there is the function @{ML fastype_of}, which + also returns the type of a term. @{ML_response [display,gray] "fastype_of (@{term \"f::nat \ bool\"} $ @{term \"x::nat\"})" "bool"} @@ -789,7 +790,7 @@ @{ML_response [display,gray] "fastype_of (@{term \"f::nat \ bool\"} $ @{term \"x::int\"})" "bool"} - where no error is raised. + where no error is detected. Sometimes it is a bit inconvenient to construct a term with complete typing annotations, especially in cases where the typing @@ -809,7 +810,7 @@ Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} Instead of giving explicitly the type for the constant @{text "plus"} and the free - variable @{text "x"}, the type-inference filled in the missing information. + variable @{text "x"}, the type-inference filles in the missing information. \begin{readmore} See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, @@ -842,7 +843,6 @@ @{ML_response_fake [display,gray] "let - val assm1 = @{cprop \"\(x::nat). P x \ Q x\"} val assm2 = @{cprop \"(P::nat\bool) t\"} @@ -916,9 +916,9 @@ text {* where the function @{ML "Thm.rule_attribute"} expects a function taking a - context (we ignore it in the code above) and a theorem (@{text thm}) and - returns another theorem (namely @{text thm} resolved with the rule - @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns + context (which we ignore in the code above) and a theorem (@{text thm}), and + returns another theorem (namely @{text thm} resolved with the lemma + @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns an attribute (of type @{ML_type "attribute"}). Before we can use the attribute, we need to set it up. This can be done @@ -931,10 +931,11 @@ *} text {* - The attribute does not expect any further arguments (like @{text "[OF \]"} that - can take a list of theorems as argument). Therefore we use the function - @{ML Attrib.no_args}. Later on we will also consider attributes taking further - arguments. An example for the attribute @{text "[my_sym]"} is the proof + The attribute does not expect any further arguments (unlike @{text "[OF + \]"}, for example, which can take a list of theorems as argument). Therefore + we use the function @{ML Attrib.no_args}. Later on we will also consider + attributes taking further arguments. An example for the attribute @{text + "[my_sym]"} is the proof *} lemma test[my_sym]: "2 = Suc (Suc 0)" by simp