# HG changeset patch # User Christian Urban # Date 1235650584 0 # Node ID 253ea99c144195fb8ff8712ac99b58f779d05f5b # Parent 84d1392186d3b27629a91adda89d9bf1e5f05ef1 polished 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 diff -r 84d1392186d3 -r 253ea99c1441 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Wed Feb 25 22:13:41 2009 +0000 +++ b/CookBook/Parsing.thy Thu Feb 26 12:16:24 2009 +0000 @@ -45,7 +45,7 @@ @{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"} - This function will either succeed (as in the two examples above) or raise the exception + The function @{ML "$$"} will either succeed (as in the two examples above) or raise the exception @{text "FAIL"} if no string can be consumed. For example trying to parse @{ML_response_fake [display,gray] "($$ \"x\") (explode \"world\")" @@ -318,14 +318,6 @@ where the single-character strings in the parsed output are transformed back into one string. - \begin{exercise}\label{ex:scancmts} - Write a parser that parses an input string so that any comment enclosed - inside @{text "(*\*)"} is replaced by a the same comment but enclosed inside - @{text "(**\**)"} in the output string. To enclose a string, you can use the - function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML - "s1 ^ s ^ s2" for s1 s2 s}. - \end{exercise} - The function @{ML Scan.ahead} parses some input, but leaves the original input unchanged. For example: @@ -342,6 +334,14 @@ "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"} (FIXME: In which situations is this useful? Give examples.) + + \begin{exercise}\label{ex:scancmts} + Write a parser that parses an input string so that any comment enclosed + inside @{text "(*\*)"} is replaced by a the same comment but enclosed inside + @{text "(**\**)"} in the output string. To enclose a string, you can use the + function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML + "s1 ^ s ^ s2" for s1 s2 s}. + \end{exercise} *} section {* Parsing Theory Syntax *} @@ -354,7 +354,7 @@ ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*} text {* - This reason for using token parsers is that theory syntax, as well as the + The reason for using token parsers is that theory syntax, as well as the parsers for the arguments of proof methods, use the type @{ML_type OuterLex.token} (which is identical to the type @{ML_type OuterParse.token}). However, there are also handy parsers for @@ -576,7 +576,7 @@ "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\"" "XML.Elem (\"token\", [], [XML.Text \"foo\"])"} - This function returns an XML-tree. You can see better what is going on if + The result of the decoding is an XML-tree. You can see better what is going on if you replace @{ML Position.none} by @{ML "Position.line 42"}, say: @{ML_response [display,gray] @@ -587,8 +587,8 @@ end" "XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"} - The positional information is stored so that code called later on will be - able to give more precise error messages. + The positional information is stored as part of an XML-tree so that code + called later on will be able to give more precise error messages. \begin{readmore} The functions to do with input and output of XML and YXML are defined @@ -692,12 +692,12 @@ *} text {* - Whenever types are given, they are stored in the @{ML SOME}s. Since types - are part of the inner syntax they are strings with some encoded information - (see previous section). - If a syntax translation is present for a variable, then it is - stored in the @{ML Mixfix} datastructure; no syntax translation is - indicated by @{ML NoSyn}. + Whenever types are given, they are stored in the @{ML SOME}s. They types are + not yet given to the variable: this must be done by type inference later + on. Since types are part of the inner syntax they are strings with some + encoded information (see previous section). If a syntax translation is + present for a variable, then it is stored in the @{ML Mixfix} datastructure; + no syntax translation is indicated by @{ML NoSyn}. \begin{readmore} The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. @@ -929,7 +929,9 @@ and then ``open up'' a proof in order to prove the proposition (for example \isacommand{lemma}) or prove some other properties (for example \isacommand{function}). To achieve this kind of behaviour, you have to use the kind - indicator @{ML thy_goal in OuterKeyword}. + indicator @{ML thy_goal in OuterKeyword}. Note, however, once you change the + ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} + then the keyword file needs to be re-created. Below we change \isacommand{foobar} so that it takes a proposition as argument and then starts a proof in order to prove it. Therefore in Line 13, @@ -981,8 +983,7 @@ \isacommand{done} \end{isabelle} - However, once you change the ``kind'' of a command from @{ML thy_decl in OuterKeyword} - to @{ML thy_goal in OuterKeyword} then the keyword file needs to be re-created. + (FIXME What do @{ML "Toplevel.theory"} @{ML "Toplevel.print"} diff -r 84d1392186d3 -r 253ea99c1441 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Wed Feb 25 22:13:41 2009 +0000 +++ b/CookBook/Tactical.thy Thu Feb 26 12:16:24 2009 +0000 @@ -311,7 +311,7 @@ "(C)"}. Since the goal @{term C} can potentially be an implication, there is a ``protector'' wrapped around it (in from of an outermost constant @{text "Const (\"prop\", bool \ bool)"}; however this constant - is invisible in the figure). This prevents that premises of @{text C} are + is invisible in the figure). This wrapper prevents that premises of @{text C} are mis-interpreted as open subgoals. While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion @{term C} intact, with the exception of possibly instantiating schematic @@ -453,7 +453,7 @@ (*<*)oops(*>*) text {* - where the application of Rule @{text bspec} generates two subgoals involving the + where the application of rule @{text bspec} generates two subgoals involving the meta-variable @{text "?x"}. Now, if you are not careful, tactics applied to the first subgoal might instantiate this meta-variable in such a way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"} @@ -576,7 +576,7 @@ \end{tabular} \end{quote} - Note in the actual output the brown colour of the variables @{term x} and + Notice in the actual output the brown colour of the variables @{term x} and @{term y}. Although they are parameters in the original goal, they are fixed inside the subproof. By convention these fixed variables are printed in brown colour. Similarly the schematic variable @{term z}. The assumption, or premise, @@ -727,12 +727,13 @@ the first goal. To do this can result in quite messy code. In contrast, the ``reverse application'' is easy to implement. - (FIXME: mention @{ML "CSUBGOAL"}) + The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes + a @{ML_type cterm} instead of a @{ML_type term}. Of course, this example is + contrived: there are much simpler methods available in Isabelle for + implementing a proof procedure analysing a goal according to its topmost + connective. These simpler methods use tactic combinators, which we will + explain in the next section. - Of course, this example is contrived: there are much simpler methods available in - Isabelle for implementing a proof procedure analysing a goal according to its topmost - connective. These simpler methods use tactic combinators, which we will explain - in the next section. *} section {* Tactic Combinators *} @@ -1027,10 +1028,10 @@ text {* In Isabelle you can also implement custom simplification procedures, called - \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and - rewrite a term according to a theorem. They are useful in cases where - a rewriting rule must be produced on ``demand'' or when rewriting by - simplification is too unpredictable and potentially loops. + \emph{simprocs}. Simprocs can be triggered by the simplifier on a specified + term-pattern and rewrite a term according to a theorem. They are useful in + cases where a rewriting rule must be produced on ``demand'' or when + rewriting by simplification is too unpredictable and potentially loops. To see how simprocs work, let us first write a simproc that just prints out the pattern which triggers it and otherwise does nothing. For this @@ -1052,7 +1053,7 @@ returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the moment we are \emph{not} interested in actually rewriting anything. We want that the simproc is triggered by the pattern @{term "Suc n"}. This can be - done by adding the simproc to the current simproc as follows + done by adding the simproc to the current simpset as follows *} simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *} @@ -1114,7 +1115,8 @@ text {* Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm} (therefore we printing it out using the function @{ML string_of_term in Syntax}). - We can turn this function into a proper simproc using + We can turn this function into a proper simproc using the function + @{ML Simplifier.simproc_i}: *} @@ -1130,7 +1132,7 @@ Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). The function also takes a list of patterns that can trigger the simproc. Now the simproc is set up and can be explicitly added using - {ML addsimprocs} to a simpset whenerver + @{ML addsimprocs} to a simpset whenerver needed. Simprocs are applied from inside to outside and from left to right. You can @@ -1138,7 +1140,7 @@ *} lemma shows "Suc (Suc 0) = (Suc 1)" - apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*}) + apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*}) (*<*)oops(*>*) text {* @@ -1190,7 +1192,7 @@ *} lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)" - apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sp]) 1*}) + apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*}) txt{* where the simproc produces the goal state @@ -1208,7 +1210,6 @@ Next let us implement a simproc that replaces terms of the form @{term "Suc n"} with the number @{text n} increase by one. First we implement a function that takes a term and produces the corresponding integer value. - *} ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t @@ -1412,7 +1413,7 @@ @{ML_response_fake [display,gray] "let - val ctrm = @{cterm \"True \ (Foo \ Bar)\"} + val ctrm = @{cterm \"True \ (Foo \ Bar)\"} in Conv.rewr_conv @{thm true_conj1} ctrm end" @@ -1439,7 +1440,8 @@ "(\x. x \ False) True \ False"} where we first beta-reduce the term and then rewrite according to - @{thm [source] true_conj1}. + @{thm [source] true_conj1}. (Recall the problem with the pretty-printer + normalising all terms.) The conversion combinator @{ML else_conv} tries out the first one, and if it does not apply, tries the second. For example @@ -1459,11 +1461,11 @@ does not fail, however, because the combinator @{ML else_conv} will then try out @{ML Conv.all_conv}, which always succeeds. - Apart from the function @{ML beta_conversion in Thm}, which able to fully - beta-normalise a term, the restriction of conversions so far is that they + Apart from the function @{ML beta_conversion in Thm}, which is able to fully + beta-normalise a term, the conversions so far are restricted in that they only apply to the outer-most level of a @{ML_type cterm}. In what follows we will lift this restriction. The combinator @{ML Conv.arg_conv} will apply - the conversion on the first argument of an application, that is the term + the conversion to the first argument of an application, that is the term must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied to @{text t2}. For example @@ -1477,7 +1479,7 @@ "P \ (True \ Q) \ P \ Q"} The reason for this behaviour is that @{text "(op \)"} expects two - arguments. So the term must be of the form @{text "Const \ $ t1 $ t2"}. The + arguments. So the term must be of the form @{text "(Const \ $ t1) $ t2"}. The conversion is then applied to @{text "t2"} which in the example above stands for @{term "True \ Q"}. @@ -1515,8 +1517,10 @@ text {* This functions descends under applications (Line 6 and 7) and abstractions (Line 8); and ``fires'' if the outer-most constant is an @{text "True \ \"} - (Lines 3-5); otherwise it leaves the term unchanged (Line 9). To see this - conversion in action, consider the following example. + (Lines 3-5); otherwise it leaves the term unchanged (Line 9). In Line 2 + we need to transform the @{ML_type cterm} into a @{ML_type term} in order + to be able to pattern-match the term. To see this + conversion in action, consider the following example @{ML_response_fake [display,gray] "let @@ -1527,9 +1531,11 @@ end" "distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} - To see how much control you have about rewriting via conversions, let us + where the conversion is applied ``deep'' inside the term. + + To see how much control you have about rewriting by using conversions, let us make the task a bit more complicated by rewriting according to the rule - @{text true_conj1}, but only in the first arguments of @{term If}s. The + @{text true_conj1}, but only in the first arguments of @{term If}s. Then the conversion should be as follows. *} @@ -1543,7 +1549,7 @@ | _ => Conv.all_conv ctrm *} text {* - Here is an application of this conversion: + Here is an example for this conversion: @{ML_response_fake [display,gray] "let @@ -1560,7 +1566,7 @@ text {* So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example, - consider @{ML all_true1_conv} and the lemma: + consider the conversion @{ML all_true1_conv} and the lemma: *} lemma foo_test: "P \ (True \ \P)" by simp @@ -1583,7 +1589,7 @@ the conclusion of a goal. Assume we want to apply @{ML all_true1_conv} only in the conclusion - of the goal, and @{ML if_true1_conv} should only be applied in the premises. + of the goal, and @{ML if_true1_conv} should only be applied to the premises. Here is a tactic doing exactly that: *} @@ -1611,9 +1617,7 @@ apply(tactic {* true1_tac 1 *}) txt {* where the tactic yields the goal state - \begin{minipage}{\textwidth} - @{subgoals [display]} - \end{minipage} *} + @{subgoals [display]}*} (*<*)oops(*>*) text {* diff -r 84d1392186d3 -r 253ea99c1441 cookbook.pdf Binary file cookbook.pdf has changed