# HG changeset patch # User Christian Urban # Date 1236988102 -3600 # Node ID 4e2341f6599dce628342a8b857bc25b73c0c56f6 # Parent 3da5f3f07d8b3dd1d517846a706da25f528f8954 polishing diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/FirstSteps.thy Sat Mar 14 00:48:22 2009 +0100 @@ -248,11 +248,35 @@ avoided: it is more than easy to get the intermediate values wrong, not to mention the nightmares the maintenance of this code causes! + A ``real world'' example for a function written in the waterfall fashion might + be the following: +*} - (FIXME: give a real world example involving theories) +ML %linenosgray{*fun apply_fresh_args pred ctxt = + pred |> fastype_of + |> binder_types + |> map (pair "z") + |> Variable.variant_frees ctxt [pred] + |> map Free + |> (curry list_comb) pred *} - Similarly, the combinator @{ML "#>"} is the reverse function - composition. It can be used to define the following function +text {* + The point of this function is to extract the argument types of the given + predicate and then generate for each type a distinct variable; finally it + applies the generated variables to the predicate. You can read this off from + how the function is coded: in Line 2, the function @{ML fastype_of} + calculates the type of the predicate; in Line 3, @{ML binder_types} produces + the list of argument types; Line 4 pairs up each type with the string/name + @{text "z"}; the function @{ML variant_frees in Variable} generates for each + @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs + is turned into a list of variable terms in Line 6, which in the last line + are applied by the function @{ML list_comb} to the predicate. We have to use + the function @{ML curry}, because @{ML list_comb} expects the predicate and + the argument list as a pair. + + + The combinator @{ML "#>"} is the reverse function composition. It can be + used to define the following function *} ML{*val inc_by_six = @@ -800,7 +824,7 @@ @{ML_response [display,gray] "fastype_of (@{term \"f::nat \ bool\"} $ @{term \"x::nat\"})" "bool"} - However, efficiency is gained on the expense of skiping some tests. You + However, efficiency is gained on the expense of skipping some tests. You can see this in the following example @{ML_response [display,gray] @@ -944,8 +968,7 @@ using the function @{ML Attrib.add_attributes} as follows. *} -setup {* - Attrib.add_attributes +setup %gray {* Attrib.add_attributes [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *} text {* @@ -1012,10 +1035,9 @@ and set up the attributes as follows *} -setup {* - Attrib.add_attributes - [("my_thms", Attrib.add_del_args my_add my_del, - "maintaining a list of my_thms")] *} +setup %gray {* Attrib.add_attributes + [("my_thms", Attrib.add_del_args my_add my_del, + "maintaining a list of my_thms")] *} text {* Now if you prove the lemma attaching the attribute @{text "[my_thms]"} @@ -1094,7 +1116,7 @@ and set up the @{ML_struct FooRules} with the command *} -setup {* FooRules.setup *} +setup %gray {* FooRules.setup *} text {* This code declares a data slot where the theorems are stored, diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/Intro.thy --- a/CookBook/Intro.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/Intro.thy Sat Mar 14 00:48:22 2009 +0100 @@ -108,7 +108,7 @@ Further information or pointers to files. \end{readmore} - A few exercises a scattered around the text. Their solutions are given + A few exercises are scattered around the text. Their solutions are given in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try to solve the exercises on your own, and then look at the solutions. diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/Package/Ind_Code.thy Sat Mar 14 00:48:22 2009 +0100 @@ -189,6 +189,8 @@ set up the goals for the induction principles. *} +ML {* singleton *} +ML {* ProofContext.export *} ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = let diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/Package/Ind_Interface.thy --- a/CookBook/Package/Ind_Interface.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/Package/Ind_Interface.thy Sat Mar 14 00:48:22 2009 +0100 @@ -139,7 +139,7 @@ in parse spec_parser input end" -"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []), +"(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), [((even0,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/Package/Simple_Inductive_Package.thy --- a/CookBook/Package/Simple_Inductive_Package.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/Package/Simple_Inductive_Package.thy Sat Mar 14 00:48:22 2009 +0100 @@ -31,7 +31,7 @@ simple_inductive accpart for r :: "'a \ 'a \ bool" where - accpartI: "(\y. r y x \ accpart r y) \ accpart r x" + accpartI: "(\y. r y x \ accpart r y) \ accpart r x" thm accpart_def thm accpart.induct @@ -53,9 +53,6 @@ thm rel.accpartI' thm rel.accpart'.induct - - -lemma "True" by simp *) use_chunks "simple_inductive_package.ML" diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/Parsing.thy --- a/CookBook/Parsing.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/Parsing.thy Sat Mar 14 00:48:22 2009 +0100 @@ -613,14 +613,6 @@ | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" -text {* and *} - -simple_inductive - trcl\ for R :: "'a \ 'a \ bool" -where - base: "trcl\ R x x" -| step: "trcl\ R x y \ R y z \ trcl\ R x z" - text {* For this we are going to use the parser: *} @@ -628,7 +620,6 @@ ML %linenosgray{*val spec_parser = OuterParse.opt_target -- OuterParse.fixes -- - OuterParse.for_fixes -- Scan.optional (OuterParse.$$$ "where" |-- OuterParse.!!! @@ -655,16 +646,16 @@ in parse spec_parser input end" -"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []), +"(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), [((even0,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} - As you see, the result is a ``nested'' four-tuple consisting of an - optional locale (in this case @{ML NONE}); a list of variables with optional - type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this - case there are none); and a list of rules where every rule has optionally a name and - an attribute. + As you see, the result is a ``nested'' four-tuple consisting of an optional + locale (in this case @{ML NONE}); a list of variables with optional + type-annotation and syntax-annotation; and a list of rules where every rule + has optionally a name and an attribute. + In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target in order to indicate a locale in which the specification is made. For example @@ -705,15 +696,7 @@ The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. \end{readmore} - Similarly, the function @{ML OuterParse.for_fixes} in Line 4: it reads the - same \isacommand{and}-separated list of variables as @{ML "fixes" in OuterParse}, - but requires that this list is prefixed by the keyword \isacommand{for}. - -@{ML_response [display,gray] -"parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")" -"([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"} - - Lines 5 to 9 in the function @{ML spec_parser} implement the parser for a + Lines 4 to 8 in the function @{ML spec_parser} implement the parser for a list of introduction rules, that is propositions with theorem annotations. The introduction rules are propositions parsed by @{ML OuterParse.prop}. However, they can include an optional theorem name plus @@ -729,7 +712,7 @@ The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name has to end with @{text [quotes] ":"}---see the argument of - the function @{ML SpecParse.opt_thm_name} in Line 9. + the function @{ML SpecParse.opt_thm_name} in Line 8. \begin{readmore} Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/Solutions.thy --- a/CookBook/Solutions.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/Solutions.thy Sat Mar 14 00:48:22 2009 +0100 @@ -79,7 +79,7 @@ text {* The setup for the simproc is *} -simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *} +simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *} text {* and a test case is the lemma *} diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/Tactical.thy --- a/CookBook/Tactical.thy Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/Tactical.thy Sat Mar 14 00:48:22 2009 +0100 @@ -524,6 +524,7 @@ text_raw{* \begin{figure}[t] +\begin{minipage}{\textwidth} \begin{isabelle} *} ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = @@ -544,6 +545,7 @@ end*} text_raw{* \end{isabelle} +\end{minipage} \caption{A function that prints out the various parameters provided by the tactic @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}} @@ -1120,6 +1122,7 @@ text_raw {* \begin{figure}[t] +\begin{minipage}{\textwidth} \begin{isabelle}*} ML{*fun print_ss ctxt ss = let @@ -1144,6 +1147,7 @@ end*} text_raw {* \end{isabelle} +\end{minipage} \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing all printable information stored in a simpset. We are here only interested in the simplifcation rules, congruence rules and simprocs.\label{fig:printss}} @@ -1455,7 +1459,7 @@ done by adding the simproc to the current simpset as follows *} -simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *} +simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *} text {* where the second argument specifies the pattern and the right-hand side @@ -1539,7 +1543,7 @@ *} lemma shows "Suc (Suc 0) = (Suc 1)" - apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*}) +apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*}) (*<*)oops(*>*) text {* @@ -1591,11 +1595,13 @@ *} lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)" - apply(tactic {* simp_tac (HOL_basic_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 - + + \begin{minipage}{\textwidth} @{subgoals[display]} + \end{minipage} *} (*<*)oops(*>*) @@ -1694,11 +1700,13 @@ *} lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))" - apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*}) +apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*}) txt {* you obtain the more legible goal state + \begin{minipage}{\textwidth} @{subgoals [display]} + \end{minipage} *} (*<*)oops(*>*) @@ -2025,7 +2033,9 @@ apply(tactic {* true1_tac 1 *}) txt {* where the tactic yields the goal state - @{subgoals [display]}*} + \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} (*<*)oops(*>*) text {* diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/document/root.tex --- a/CookBook/document/root.tex Fri Mar 13 16:57:16 2009 +0100 +++ b/CookBook/document/root.tex Sat Mar 14 00:48:22 2009 +0100 @@ -97,6 +97,10 @@ \renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}} \renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}} +\isakeeptag{gray} +\renewcommand{\isataggray}{\begin{graybox}} +\renewcommand{\endisataggray}{\end{graybox}} + \isakeeptag{small} \renewcommand{\isatagsmall}{\begingroup\small} \renewcommand{\endisatagsmall}{\endgroup} diff -r 3da5f3f07d8b -r 4e2341f6599d cookbook.pdf Binary file cookbook.pdf has changed