--- a/ProgTutorial/FirstSteps.thy Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Sat Nov 07 01:03:37 2009 +0100
@@ -91,6 +91,9 @@
However, both commands will only play minor roles in this tutorial (we will
always arrange that the ML-code is defined outside proofs).
+
+
+
Once a portion of code is relatively stable, you usually want to export it
to a separate ML-file. Such files can then be included somewhere inside a
theory by using the command \isacommand{use}. For example
@@ -542,8 +545,27 @@
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.
+ composition allows you to read the code top-down. This combinator is often used
+ for setup function inside the \isacommand{setup}-command. These function have to be
+ of type @{ML_type "theory -> theory"} in order to install, for example, some new
+ data inside the current theory. More than one such setup function can be composed
+ with @{ML "#>"}. For example
+*}
+setup %gray {* let
+ val (ival1, setup_ival1) = Attrib.config_int "ival1" 1
+ val (ival2, setup_ival2) = Attrib.config_int "ival2" 2
+in
+ setup_ival1 #>
+ setup_ival2
+end *}
+
+text {*
+ after this the configuration values @{text ival1} and @{text ival2} are known
+ in the current theory and can be manipulated by the user (for more information
+ about configuration values see Section~\ref{sec:storing}, for more about setup
+ functions see Section~\ref{sec:theories}).
+
The remaining combinators we describe in this section add convenience for the
``waterfall method'' of writing functions. The combinator @{ML_ind tap in
Basics} allows you to get hold of an intermediate result (to do some
@@ -814,6 +836,21 @@
under this name (this becomes especially important when you deal with
theorem lists; see Section \ref{sec:storing}).
+ It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
+ whose first argument is a statement (possibly many of them separated by @{text "and"},
+ and the second is a proof. For example
+*}
+
+ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *}
+
+text {*
+ which can be printed out as follows
+
+ @{ML_response_fake [gray,display]
+"foo_thm |> string_of_thms @{context}
+ |> tracing"
+ "True, True"}
+
You can also refer to the current simpset via an antiquotation. To illustrate
this we implement the function that extracts the theorem names stored in a
simpset.
--- a/ProgTutorial/General.thy Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/General.thy Sat Nov 07 01:03:37 2009 +0100
@@ -174,15 +174,87 @@
text {*
Like with terms, there is the distinction between free type
variables (term-constructor @{ML "TFree"}) and schematic
- type variables (term-constructor @{ML "TVar"}). A type constant,
+ type variables (term-constructor @{ML "TVar"} and printed with
+ a leading question mark). A type constant,
like @{typ "int"} or @{typ bool}, are types with an empty list
- of argument types. However, it is a bit difficult to show an
- example, because Isabelle always pretty-prints types (unlike terms).
- Here is a contrived example:
+ of argument types. However, it needs a bit of effort to show an
+ example, because Isabelle always pretty prints types (unlike terms).
+ Using just the antiquotation @{text "@{typ \"bool\"}"} we only see
@{ML_response [display, gray]
- "if Type (\"bool\", []) = @{typ \"bool\"} then true else false"
- "true"}
+ "@{typ \"bool\"}"
+ "bool"}
+
+ the pretty printed version of @{text "bool"}. However, in PolyML it is
+ easy to install your own pretty printer. With the function below we
+ mimic the behaviour of the usual pretty printer for
+ datatypes.\footnote{Thanks to David Matthews for providing this
+ code.}
+*}
+
+ML{*fun typ_raw_pretty_printer depth _ ty =
+let
+ fun cond str a =
+ if depth <= 0
+ then PolyML.PrettyString "..."
+ else PolyML.PrettyBlock(1, false, [],
+ [PolyML.PrettyString str, PolyML.PrettyBreak(1, 0), a])
+in
+ case ty of
+ Type a => cond "Type" (PolyML.prettyRepresentation(a, depth - 1))
+ | TFree a => cond "TFree" (PolyML.prettyRepresentation(a, depth - 1))
+ | TVar a => cond "TVar" (PolyML.prettyRepresentation(a, depth - 1))
+end*}
+
+text {*
+ We can install this pretty printer with the function
+ @{ML_ind addPrettyPrinter in PolyML} as follows.
+*}
+
+ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
+
+text {*
+ Now the type bool is printed out as expected.
+
+ @{ML_response [display,gray]
+ "@{typ \"bool\"}"
+ "Type (\"bool\", [])"}
+
+ When printing out a list-type
+
+ @{ML_response [display,gray]
+ "@{typ \"'a list\"}"
+ "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
+
+ we can see the full name of the type is actually @{text "List.list"}, indicating
+ that it is defined in the theory @{text "List"}. However, one has to be
+ careful with finding out the right name of a type, because even if
+ @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the
+ theories @{text "HOL"} and @{text "Nat"}, respectively, they are
+ still represented by their simple name.
+
+ @{ML_response [display,gray]
+ "@{typ \"bool \<Rightarrow> nat\"}"
+ "Type (\"fun\", [Type (\"bool\", []), Type (\"nat\", [])])"}
+
+ We can restore the usual behaviour of Isabelle's pretty printer
+ with the code
+*}
+
+ML{*fun stnd_pretty_printer _ _ =
+ ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy;
+
+PolyML.addPrettyPrinter stnd_pretty_printer*}
+
+text {*
+ After that the types for booleans, lists and so on are printed out again
+ the standard Isabelle way.
+
+ @{ML_response_fake [display, gray]
+ "@{typ \"bool\"};
+@{typ \"'a list\"}"
+ "\"bool\"
+\"'a List.list\""}
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
@@ -1119,14 +1191,14 @@
consisting of a name and a kind. When we store lemmas in the theorem database,
we might want to explicitly extend this data by attaching case names to the
- two premises of the lemma. This can be done with the function @{ML_ind name in RuleCases}
- from the structure @{ML_struct RuleCases}.
+ two premises of the lemma. This can be done with the function @{ML_ind name in Rule_Cases}
+ from the structure @{ML_struct Rule_Cases}.
*}
local_setup %gray {*
LocalTheory.note Thm.lemmaK
((@{binding "foo_data'"}, []),
- [(RuleCases.name ["foo_case_one", "foo_case_two"]
+ [(Rule_Cases.name ["foo_case_one", "foo_case_two"]
@{thm foo_data})]) #> snd *}
text {*
--- a/ProgTutorial/Package/Ind_Code.thy Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy Sat Nov 07 01:03:37 2009 +0100
@@ -1005,8 +1005,8 @@
||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins)
||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules)
||>> fold_map (note_single2 @{binding "induct"}
- [Attrib.internal (K (RuleCases.case_names case_names)),
- Attrib.internal (K (RuleCases.consumes 1)),
+ [Attrib.internal (K (Rule_Cases.case_names case_names)),
+ Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))])
(prednames ~~ ind_prins)
|> snd
@@ -1043,9 +1043,9 @@
Line 20 add further every introduction rule under its own name
(given by the user).\footnote{FIXME: what happens if the user did not give
any name.} Line 21 registers the induction principles. For this we have
- to use some specific attributes. The first @{ML_ind case_names in RuleCases}
+ to use some specific attributes. The first @{ML_ind case_names in Rule_Cases}
corresponds to the case names that are used by Isar to reference the proof
- obligations in the induction. The second @{ML "consumes 1" in RuleCases}
+ obligations in the induction. The second @{ML "consumes 1" in Rule_Cases}
indicates that the first premise of the induction principle (namely
the predicate over which the induction proceeds) is eliminated.
--- a/ProgTutorial/Package/simple_inductive_package.ML Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML Sat Nov 07 01:03:37 2009 +0100
@@ -187,8 +187,8 @@
|>> snd
||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
- [Attrib.internal (K (RuleCases.case_names case_names)),
- Attrib.internal (K (RuleCases.consumes 1)),
+ [Attrib.internal (K (Rule_Cases.case_names case_names)),
+ Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
(preds ~~ inducts)) #>> maps snd)
|> snd
Binary file progtutorial.pdf has changed