--- a/CookBook/Appendix.thy Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/Appendix.thy Mon Feb 23 00:27:27 2009 +0000
@@ -7,12 +7,17 @@
text {*
Possible topics: translations/print translations
-
*}
chapter {* Recipes *}
+text {*
+ Possible topics: translations/print translations
+
+ User Space Type Systems (in the already existing form)
+*}
+
end
--- a/CookBook/FirstSteps.thy Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/FirstSteps.thy Mon Feb 23 00:27:27 2009 +0000
@@ -171,7 +171,7 @@
section {* Combinators\label{sec:combinators} *}
text {*
- For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
+ 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.
@@ -213,7 +213,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 Haskell's do-notation. Writing the function @{ML inc_by_five} using
+ if you used to Haskell's do-notation. Writing the function @{ML inc_by_five} using
the reverse application is much clearer than writing
*}
@@ -380,23 +380,28 @@
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
- and current simpsets:
+ and current simpsets. For this we use the function that extracts the
+ theorem names stored in the simpset.
+*}
- @{ML_response_fake [display,gray]
-"let
- val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset}
+ML{*fun get_thm_names simpset =
+let
+ val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
in
map #name (Net.entries rules)
-end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+end*}
- The code about simpsets extracts the theorem names stored in the
- 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
- indexing). From this net you can extract the entries using the function @{ML
- Net.entries}.
+text {*
+ 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 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 of
+ the current simpset using the antiquotation @{text "@{simpset}"}.\footnote
+ {FIXME: you cannot cleanly match against lists with ommited parts}
+ @{ML_response_fake [display,gray]
+"get_thm_names @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
\begin{readmore}
The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
@@ -511,11 +516,11 @@
*}
ML{*fun make_imp P Q tau =
- let
- val x = Free ("x",tau)
- in
- Logic.all x (Logic.mk_implies (P $ x, Q $ x))
- end *}
+let
+ val x = Free ("x",tau)
+in
+ Logic.all x (Logic.mk_implies (P $ x, Q $ x))
+end *}
text {*
The reason is that you cannot pass the arguments @{term P}, @{term Q} and
@@ -603,7 +608,7 @@
There are a few subtle issues with constants. They usually crop up when
- pattern matching terms or constructing terms. While it is perfectly ok
+ pattern matching terms or types, or constructing them. While it is perfectly ok
to write the function @{text is_true} as follows
*}
@@ -637,10 +642,10 @@
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
- matches correctly (the wildcard in the pattern matches any type).
+ matches correctly (the first wildcard in the pattern matches any type).
However there is still a problem: consider the similar function that
- attempts to pick out a @{text "Nil"}-term:
+ attempts to pick out @{text "Nil"}-terms:
*}
ML{*fun is_nil (Const ("Nil", _)) = true
@@ -658,11 +663,11 @@
@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
- the name of the constant @{term "Nil"} depends on the theory in which the
+ the name of the constant @{text "Nil"} depends on the theory in which the
term constructor is defined (@{text "List"}) and also in which datatype
(@{text "list"}). Even worse, some constants have a name involving
type-classes. Consider for example the constants for @{term "zero"} and
- @{text "(op *)"}:
+ \mbox{@{text "(op *)"}}:
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
"(Const (\"HOL.zero_class.zero\", \<dots>),
@@ -684,7 +689,7 @@
| is_nil_or_all _ = false *}
text {*
- Note that you occasional have to calculate what the ``base'' name of a given
+ Occasional you have to calculate what the ``base'' name of a given
constant is. For this you can use the function @{ML Sign.extern_const} or
@{ML Sign.base_name}. For example:
@@ -694,8 +699,6 @@
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)
-
\begin{readmore}
FIXME
\end{readmore}
@@ -706,15 +709,15 @@
text {*
- You can freely construct and manipulate @{ML_type "term"}s, since they are just
- arbitrary unchecked trees. However, you eventually want to see if a
- term is well-formed, or type-checks, relative to a theory.
- Type-checking is done via the function @{ML cterm_of}, which converts
- a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
- Unlike @{ML_type term}s, which are just trees, @{ML_type
- "cterm"}s are abstract objects that are guaranteed to be
- type-correct, and they can only be constructed via ``official
- interfaces''.
+ You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
+ typ}es, since they are just arbitrary unchecked trees. However, you
+ eventually want to see if a term is well-formed, or type-checks, relative to
+ a theory. Type-checking is done via the function @{ML cterm_of}, which
+ converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
+ term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
+ abstract objects that are guaranteed to be type-correct, and they can only
+ be constructed via ``official interfaces''.
+
Type-checking is always relative to a theory context. For now we use
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
@@ -765,7 +768,7 @@
"*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
Since the complete traversal might sometimes be too costly and
- not necessary, there is also the function @{ML fastype_of} which
+ not necessary, there is also the function @{ML fastype_of}, which
returns the type of a term.
@{ML_response [display,gray]
@@ -799,7 +802,6 @@
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.
-
\begin{readmore}
See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
checking and pretty-printing of terms are defined.
--- a/CookBook/Parsing.thy Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/Parsing.thy Mon Feb 23 00:27:27 2009 +0000
@@ -45,11 +45,6 @@
@{ML_response [display,gray] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
- The type of a parser is defined as
-
-
-
-
This function 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
@@ -581,8 +576,8 @@
"YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
"XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
- You can see better what is going on if you replace
- @{ML Position.none} by @{ML "Position.line 42"}, say:
+ This function returns 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]
"let
@@ -663,7 +658,7 @@
((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
- As can be seen, the result is a ``nested'' four-tuple consisting of an
+ 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
@@ -716,9 +711,10 @@
"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 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
+ Lines 5 to 9 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
some attributes. For example
@{ML_response [display,gray] "let
@@ -729,8 +725,8 @@
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
- @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some
- attributes. The name has to end with @{text [quotes] ":"}---see argument of
+ @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name
+ has to end with @{text [quotes] ":"}---see the argument of
@{ML SpecParse.opt_thm_name} in Line 9.
\begin{readmore}
--- a/CookBook/ROOT.ML Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/ROOT.ML Mon Feb 23 00:27:27 2009 +0000
@@ -24,6 +24,7 @@
use_thy "Recipes/ExternalSolver";
use_thy "Recipes/Oracle";
use_thy "Recipes/Sat";
+use_thy "Recipes/USTypes";
use_thy "Solutions";
use_thy "Readme";
--- a/CookBook/Tactical.thy Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/Tactical.thy Mon Feb 23 00:27:27 2009 +0000
@@ -798,7 +798,7 @@
*}
-ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
+ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
text {*
will first try out whether rule @{text disjI} applies and after that
@@ -1059,13 +1059,13 @@
text {*
where the second argument specifies the pattern and the right-hand side
contains the code of the simproc (we have to use @{ML K} since we ignoring
- an argument about a morphism\footnote{FIXME: what does the morphism do?}).
+ an argument about morphisms\footnote{FIXME: what does the morphism do?}).
After this, the simplifier is aware of the simproc and you can test whether
- it fires on the lemma
+ it fires on the lemma:
*}
lemma shows "Suc 0 = 1"
-apply(simp)
+ apply(simp)
(*<*)oops(*>*)
text {*
@@ -1074,8 +1074,9 @@
simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
0"}, and then the simproc ``fires'' also on that term.
- We can add or delete the simproc by the usual \isacommand{declare}-statement.
- For example the simproc will be deleted if you type:
+ We can add or delete the simproc from the current simpset by the usual
+ \isacommand{declare}-statement. For example the simproc will be deleted
+ if you type:
*}
declare [[simproc del: fail_sp]]
@@ -1087,13 +1088,14 @@
*}
lemma shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
+ apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
(*<*)oops(*>*)
text {*
(FIXME: should one use HOL-basic-ss or HOL-ss?)
- Now the message shows up only once since @{term "1::nat"} is left unchanged.
+ Now the message shows up only once since the term @{term "1::nat"} is
+ left unchanged.
Setting up a simproc using the command \isacommand{setup\_simproc} will
always add automatically the simproc to the current simpset. If you do not
@@ -1133,18 +1135,18 @@
*}
lemma shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
+ apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
(*<*)oops(*>*)
text {*
- since the @{ML fail_sp'}-simproc prints out the sequence
+ since @{ML fail_sp'} prints out the sequence
@{text [display]
"> Suc 0
> Suc (Suc 0)
> Suc 1"}
- To see how a simproc applies a theorem let us implement a simproc that
+ To see how a simproc applies a theorem, let us implement a simproc that
rewrites terms according to the equation:
*}
@@ -1153,12 +1155,13 @@
text {*
Simprocs expect that the given equation is a meta-equation, however the
- equation can contain preconditions (the simproc then will only fire if the
- preconditions can be solved). To see how rewriting can be tuned precisely, let us
- further assume we want that the simproc only rewrites terms greater than
- @{term "Suc 0"}. For this we can write
+ equation can contain preconditions (the simproc then will only fire if the
+ preconditions can be solved). To see one has relatively precise control over
+ the rewriting with simprocs, let us further assume we want that the simproc
+ only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write
*}
+
ML{*fun plus_one_sp_aux ss redex =
case redex of
@{term "Suc 0"} => NONE
@@ -1177,23 +1180,23 @@
end*}
text {*
- Now the have set up the simproc so that it is triggered by terms
+ Now the simproc is set up xso that it is triggered by terms
of the form @{term "Suc n"}, but inside the simproc we only produce
a theorem if the term is not @{term "Suc 0"}. The result you can see
- in the following proof.
+ in the following proof
*}
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_ss addsimprocs [plus_one_sp]) 1*})
txt{*
- the simproc produces the goal state
+ where the simproc produces the goal state
@{subgoals[display]}
*}
(*<*)oops(*>*)
text {*
- As usual with simplification you have to be careful with loops: you already have
+ As usual with simplification you have to be careful with looping: you already have
one @{ML plus_one_sp}, if you apply if with the default simpset (because
the default simpset contains a rule which just undoes the rewriting
@{ML plus_one_sp}).
@@ -1210,9 +1213,9 @@
text {*
It uses the library function @{ML dest_number in HOLogic} that transforms
(Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
- on, into integer values. This function raises the exception @{ML TERM} if
+ on, into integer values. This function raises the exception @{ML TERM}, if
the term is not a number. The next function expects a pair consisting of a term
- @{text t} and the corresponding integer value @{text n}.
+ @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}.
*}
ML %linenosgray{*fun get_thm ctxt (t, n) =
@@ -1224,10 +1227,12 @@
end*}
text {*
- From the integer value it generates the corresponding Isabelle term, called
- @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4)
+ (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
+
+ From the integer value it generates the corresponding number term, called
+ @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4),
which it proves by simplification in Line 6. The function @{ML mk_meta_eq}
- at the outside of the proof just transforms the equality to a meta-equality.
+ at the outside of the proof just transforms the equality into a meta-equality.
Both functions can be stringed together in the function that produces the
actual theorem for the simproc.
@@ -1242,12 +1247,10 @@
end*}
text {*
- (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
-
This function uses the fact that @{ML dest_suc_trm} might throw an exception
@{ML TERM}. In this case there is nothing that can be rewritten and therefore no
- theorem is produced. To try out the simproc on an example, you can set it up as
- follows:
+ theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc
+ on an example, you can set it up as follows:
*}
ML{*val nat_number_sp =
Binary file cookbook.pdf has changed