--- a/CookBook/FirstSteps.thy Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/FirstSteps.thy Thu Feb 19 14:44:53 2009 +0000
@@ -62,7 +62,7 @@
*}
-section {* Debugging and Printing *}
+section {* Debugging and Printing\label{sec:printing} *}
text {*
@@ -118,9 +118,230 @@
"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}
- and @{ML_type thm}.
+ Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
+ or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
+ but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
+ a term into a string is to use the function @{ML Syntax.string_of_term}.
+
+ @{ML_response_fake [display,gray]
+ "Syntax.string_of_term @{context} @{term \"1::nat\"}"
+ "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
+
+ This produces a string with some additional information encoded in it. The string
+ can be properly printed by using the function @{ML warning}.
+
+ @{ML_response_fake [display,gray]
+ "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+ "\"1\""}
+
+ A @{ML_type cterm} can be transformed into a string by the following function.
+*}
+
+ML{*fun str_of_cterm ctxt t =
+ Syntax.string_of_term ctxt (term_of t)*}
+
+text {*
+ 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 =
+ commas (map (str_of_cterm ctxt) ts)*}
+
+text {*
+ The easiest way to get the string of a theorem is to transform it
+ into a @{ML_type cterm} using the function @{ML crep_thm}.
+*}
+
+ML{*fun str_of_thm ctxt thm =
+ let
+ val {prop, ...} = crep_thm thm
+ in
+ str_of_cterm ctxt prop
+ end*}
+
+text {*
+ Again the function @{ML commas} helps with printing more than one theorem.
+*}
+
+ML{*fun str_of_thms ctxt thms =
+ commas (map (str_of_thm ctxt) thms)*}
+
+
+section {* Combinators\label{sec:combinators} *}
+
+text {*
+ (FIXME: maybe move before antiquotation section)
+
+ For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
+ the combinators. At first they seem to greatly obstruct the
+ comprehension of the code, but after getting familiar with them, they
+ actually ease the understanding and also the programming.
+
+ \begin{readmore}
+ The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+ and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
+ contains further information about combinators.
+ \end{readmore}
+
+ The simplest combinator is @{ML I}, which is just the identity function defined as
+*}
+
+ML{*fun I x = x*}
+
+text {* Another simple combinator is @{ML K}, defined as *}
+
+ML{*fun K x = fn _ => x*}
+
+text {*
+ @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
+ function ignores its argument. As a result, @{ML K} defines a constant function
+ always returning @{text x}.
+
+ The next combinator is reverse application, @{ML "|>"}, defined as:
+*}
+
+ML{*fun x |> f = f x*}
+
+text {* While just syntactic sugar for the usual function application,
+ the purpose of this combinator is to implement functions in a
+ ``waterfall fashion''. Consider for example the function *}
+
+ML %linenosgray{*fun inc_by_five x =
+ x |> (fn x => x + 1)
+ |> (fn x => (x, x))
+ |> fst
+ |> (fn x => x + 4)*}
+
+text {*
+ which increments its argument @{text x} by 5. It does this by first incrementing
+ the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
+ the first component of the pair (Line 4) and finally incrementing the first
+ component by 4 (Line 5). This kind of cascading manipulations of values is quite
+ 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 Haskell's do-notation. Writing the function @{ML inc_by_five} using
+ the reverse application is much clearer than writing
+*}
+
+ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
+
+text {* or *}
+
+ML{*fun inc_by_five x =
+ ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
+
+text {* and typographically more economical than *}
+
+ML{*fun inc_by_five x =
+ let val y1 = x + 1
+ val y2 = (y1, y1)
+ val y3 = fst y2
+ val y4 = y3 + 4
+ in y4 end*}
+
+text {*
+ Another reason why the let-bindings in the code above are better to be
+ avoided: it is more than easy to get the intermediate values wrong, not to
+ mention the nightmares the maintenance of this code causes!
+
+
+ (FIXME: give a real world example involving theories)
+
+ Similarly, the combinator @{ML "#>"} is the reverse function
+ composition. It can be used to define the following function
+*}
+
+ML{*val inc_by_six =
+ (fn x => x + 1)
+ #> (fn x => x + 2)
+ #> (fn x => x + 3)*}
+
+text {*
+ which is the function composed of first the increment-by-one function and then
+ increment-by-two, followed by increment-by-three. Again, the reverse function
+ composition allows you to read the code top-down.
+
+ The remaining combinators described in this section add convenience for the
+ ``waterfall method'' of writing functions. The combinator @{ML tap} allows
+ you to get hold of an intermediate result (to do some side-calculations for
+ instance). The function
+
+ *}
+
+ML %linenosgray{*fun inc_by_three x =
+ x |> (fn x => x + 1)
+ |> tap (fn x => tracing (makestring x))
+ |> (fn x => x + 2)*}
+
+text {*
+ increments the argument first by @{text "1"} and then by @{text "2"}. In the
+ middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
+ intermediate result inside the tracing buffer. The function @{ML tap} can
+ only be used for side-calculations, because any value that is computed
+ cannot be merged back into the ``main waterfall''. To do this, you can use
+ the next combinator.
+
+ The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
+ and returns the result together with the value (as a pair). For example
+ the function
+*}
+
+ML{*fun inc_as_pair x =
+ x |> `(fn x => x + 1)
+ |> (fn (x, y) => (x, y + 1))*}
+
+text {*
+ takes @{text x} as argument, and then increments @{text x}, but also keeps
+ @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+ for x}. After that, the function increments the right-hand component of the
+ pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
+
+ The combinators @{ML "|>>"} and @{ML "||>"} are defined for
+ functions manipulating pairs. The first applies the function to
+ the first component of the pair, defined as
+*}
+
+ML{*fun (x, y) |>> f = (f x, y)*}
+
+text {*
+ and the second combinator to the second component, defined as
+*}
+
+ML{*fun (x, y) ||> f = (x, f y)*}
+
+text {*
+ With the combinator @{ML "|->"} you can re-combine the elements from a pair.
+ This combinator is defined as
+*}
+
+ML{*fun (x, y) |-> f = f x y*}
+
+text {* and can be used to write the following roundabout version
+ of the @{text double} function:
+*}
+
+ML{*fun double x =
+ x |> (fn x => (x, x))
+ |-> (fn x => fn y => x + y)*}
+
+text {*
+ Recall that @{ML "|>"} is the reverse function applications. Recall also that the related
+ reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
+ @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
+ composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"},
+ for example, the function @{text double} can also be written as:
+*}
+
+ML{*val double =
+ (fn x => (x, x))
+ #-> (fn x => fn y => x + y)*}
+
+text {*
+
+ (FIXME: find a good exercise for combinators)
+
*}
@@ -212,7 +433,7 @@
@{ML_response [display,gray]
"@{term \"(a::nat) + b = c\"}"
"Const (\"op =\", \<dots>) $
- (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
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
@@ -256,8 +477,9 @@
inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
Consider for example the pairs
- @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
- Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
+"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
+ Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
where a coercion is inserted in the second component and
@@ -445,7 +667,7 @@
and @{text "(op *)"}:
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
- "(Const (\"HOL.zero_class.zero\", \<dots>),
+ "(Const (\"HOL.zero_class.zero\", \<dots>),
Const (\"HOL.times_class.times\", \<dots>))"}
While you could use the complete name, for example
@@ -471,7 +693,7 @@
@{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
The difference between both functions is that @{ML extern_const in Sign} returns
- the smallest name which is still unique, while @{ML base_name in Sign} always
+ the smallest name that is still unique, whereas @{ML base_name in Sign} always
strips off all qualifiers.
(FIXME authentic syntax on the ML-level)
@@ -567,13 +789,14 @@
@{ML_response_fake [display,gray]
"let
- val term =
- Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT)
+ val c = Const (@{const_name \"plus\"}, dummyT)
+ val o = @{term \"1::nat\"}
+ val v = Free (\"x\", dummyT)
in
- Syntax.check_term @{context} term
+ Syntax.check_term @{context} (c $ o $ v)
end"
- "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
- Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
+"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
+ 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 will fill in the missing information.
@@ -654,240 +877,36 @@
(FIXME: how to add case-names to goal states)
*}
-section {* Printing Terms and Theorems\label{sec:printing} *}
-
-text {*
- During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm}
- or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
- but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
- a term into a string is to use the function @{ML Syntax.string_of_term}.
-
- @{ML_response_fake [display,gray]
- "Syntax.string_of_term @{context} @{term \"1::nat\"}"
- "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
-
- This produces a string with some printing directions encoded in it. The string
- can be properly printed by using the function @{ML warning}.
-
- @{ML_response_fake [display,gray]
- "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
- "\"1\""}
-
- A @{ML_type cterm} can be transformed into a string by the following function.
-*}
-
-ML{*fun str_of_cterm ctxt t =
- Syntax.string_of_term ctxt (term_of t)*}
-
-text {*
- 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 =
- commas (map (str_of_cterm ctxt) ts)*}
-
-text {*
- The easiest way to get the string of a theorem is to transform it
- into a @{ML_type cterm} using the function @{ML crep_thm}.
-*}
-
-ML{*fun str_of_thm ctxt thm =
- let
- val {prop, ...} = crep_thm thm
- in
- str_of_cterm ctxt prop
- end*}
-
-text {*
- Again the function @{ML commas} helps with printing more than one theorem.
-*}
-
-ML{*fun str_of_thms ctxt thms =
- commas (map (str_of_thm ctxt) thms)*}
section {* Theorem Attributes *}
section {* Theories and Local Theories *}
+text {*
+ (FIXME: expand)
+
+ There are theories, proof contexts and local theories (in this order, if you
+ want to order them).
+
+ In contrast to an ordinary theory, which simply consists of a type
+ signature, as well as tables for constants, axioms and theorems, a local
+ theory also contains additional context information, such as locally fixed
+ variables and local assumptions that may be used by the package. The type
+ @{ML_type local_theory} is identical to the type of \emph{proof contexts}
+ @{ML_type "Proof.context"}, although not every proof context constitutes a
+ valid local theory.
+
+ *}
+
+
+
section {* Storing Theorems *}
text {* @{ML PureThy.add_thms_dynamic} *}
-section {* Combinators\label{sec:combinators} *}
-text {*
- For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
- the combinators. At first they seem to greatly obstruct the
- comprehension of the code, but after getting familiar with them, they
- actually ease the understanding and also the programming.
-
- \begin{readmore}
- The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
- and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
- contains further information about combinators.
- \end{readmore}
-
- The simplest combinator is @{ML I}, which is just the identity function defined as
-*}
-
-ML{*fun I x = x*}
-
-text {* Another simple combinator is @{ML K}, defined as *}
-
-ML{*fun K x = fn _ => x*}
-
-text {*
- @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
- function ignores its argument. As a result, @{ML K} defines a constant function
- always returning @{text x}.
-
- The next combinator is reverse application, @{ML "|>"}, defined as:
-*}
-
-ML{*fun x |> f = f x*}
-
-text {* While just syntactic sugar for the usual function application,
- the purpose of this combinator is to implement functions in a
- ``waterfall fashion''. Consider for example the function *}
-
-ML %linenosgray{*fun inc_by_five x =
- x |> (fn x => x + 1)
- |> (fn x => (x, x))
- |> fst
- |> (fn x => x + 4)*}
-
-text {*
- which increments its argument @{text x} by 5. It does this by first incrementing
- the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
- the first component of the pair (Line 4) and finally incrementing the first
- component by 4 (Line 5). This kind of cascading manipulations of values is quite
- 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 Haskell's do-notation. Writing the function @{ML inc_by_five} using
- the reverse application is much clearer than writing
-*}
-
-ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
-
-text {* or *}
-
-ML{*fun inc_by_five x =
- ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
-
-text {* and typographically more economical than *}
-
-ML{*fun inc_by_five x =
- let val y1 = x + 1
- val y2 = (y1, y1)
- val y3 = fst y2
- val y4 = y3 + 4
- in y4 end*}
-
-text {*
- Another reason why the let-bindings in the code above are better to be
- avoided: it is more than easy to get the intermediate values wrong, not to
- mention the nightmares the maintenance of this code causes!
-
-
- (FIXME: give a real world example involving theories)
-
- Similarly, the combinator @{ML "#>"} is the reverse function
- composition. It can be used to define the following function
-*}
-
-ML{*val inc_by_six =
- (fn x => x + 1)
- #> (fn x => x + 2)
- #> (fn x => x + 3)*}
-
-text {*
- which is the function composed of first the increment-by-one function and then
- increment-by-two, followed by increment-by-three. Again, the reverse function
- composition allows you to read the code top-down.
-
- The remaining combinators described in this section add convenience for the
- ``waterfall method'' of writing functions. The combinator @{ML tap} allows
- you to get hold of an intermediate result (to do some side-calculations for
- instance). The function
-
- *}
-
-ML %linenosgray{*fun inc_by_three x =
- x |> (fn x => x + 1)
- |> tap (fn x => tracing (makestring x))
- |> (fn x => x + 2)*}
-
-text {*
- increments the argument first by @{text "1"} and then by @{text "2"}. In the
- middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
- intermediate result inside the tracing buffer. The function @{ML tap} can
- only be used for side-calculations, because any value that is computed
- cannot be merged back into the ``main waterfall''. To do this, you can use
- the next combinator.
-
- The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
- and returns the result together with the value (as a pair). For example
- the function
-*}
-
-ML{*fun inc_as_pair x =
- x |> `(fn x => x + 1)
- |> (fn (x, y) => (x, y + 1))*}
-
-text {*
- takes @{text x} as argument, and then increments @{text x}, but also keeps
- @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
- for x}. After that, the function increments the right-hand component of the
- pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
-
- The combinators @{ML "|>>"} and @{ML "||>"} are defined for
- functions manipulating pairs. The first applies the function to
- the first component of the pair, defined as
-*}
-
-ML{*fun (x, y) |>> f = (f x, y)*}
-
-text {*
- and the second combinator to the second component, defined as
-*}
-
-ML{*fun (x, y) ||> f = (x, f y)*}
-
-text {*
- With the combinator @{ML "|->"} you can re-combine the elements from a pair.
- This combinator is defined as
-*}
-
-ML{*fun (x, y) |-> f = f x y*}
-
-text {* and can be used to write the following roundabout version
- of the @{text double} function:
-*}
-
-ML{*fun double x =
- x |> (fn x => (x, x))
- |-> (fn x => fn y => x + y)*}
-
-text {*
- Recall that @{ML "|>"} is the reverse function applications. Recall also that the related
- reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
- @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
- composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"},
- for example, the function @{text double} can also be written as:
-*}
-
-ML{*val double =
- (fn x => (x, x))
- #-> (fn x => fn y => x + y)*}
-
-text {*
-
- (FIXME: find a good exercise for combinators)
-*}
-
+(* FIXME: some code below *)
(*<*)
setup {*