--- a/ProgTutorial/FirstSteps.thy Sat May 09 18:50:01 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sun May 17 16:22:27 2009 +0200
@@ -9,14 +9,14 @@
in Isabelle is part of a theory. If you want to follow the code given in
this chapter, we assume you are working inside the theory starting with
- \begin{center}
+ \begin{quote}
\begin{tabular}{@ {}l}
\isacommand{theory} FirstSteps\\
\isacommand{imports} Main\\
\isacommand{begin}\\
\ldots
\end{tabular}
- \end{center}
+ \end{quote}
We also generally assume you are working with HOL. The given examples might
need to be adapted if you work in a different logic.
@@ -59,7 +59,7 @@
to a separate ML-file. Such files can then be included somewhere inside a
theory by using the command \isacommand{use}. For example
- \begin{center}
+ \begin{quote}
\begin{tabular}{@ {}l}
\isacommand{theory} FirstSteps\\
\isacommand{imports} Main\\
@@ -69,13 +69,13 @@
\isacommand{use}~@{text "\"file_to_be_included.ML\""}\\
\ldots
\end{tabular}
- \end{center}
+ \end{quote}
The \isacommand{uses}-command in the header of the theory is needed in order
to indicate the dependency of the theory on the ML-file. Alternatively, the
file can be included by just writing in the header
- \begin{center}
+ \begin{quote}
\begin{tabular}{@ {}l}
\isacommand{theory} FirstSteps\\
\isacommand{imports} Main\\
@@ -83,7 +83,7 @@
\isacommand{begin}\\
\ldots
\end{tabular}
- \end{center}
+ \end{quote}
Note that no parentheses are given this time.
*}
@@ -181,7 +181,7 @@
A @{ML_type cterm} can be transformed into a string by the following function.
*}
-ML{*fun str_of_cterm ctxt t =
+ML{*fun string_of_cterm ctxt t =
Syntax.string_of_term ctxt (term_of t)*}
text {*
@@ -190,23 +190,23 @@
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)*}
+ML{*fun string_of_cterms ctxt ts =
+ commas (map (string_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 =
- str_of_cterm ctxt (#prop (crep_thm thm))*}
+ML{*fun string_of_thm ctxt thm =
+ string_of_cterm ctxt (#prop (crep_thm thm))*}
text {*
Theorems also include schematic variables, such as @{text "?P"},
@{text "?Q"} and so on.
@{ML_response_fake [display, gray]
- "writeln (str_of_thm @{context} @{thm conjI})"
+ "writeln (string_of_thm @{context} @{thm conjI})"
"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
In order to improve the readability of theorems we convert
@@ -221,30 +221,28 @@
thm'
end
-fun str_of_thm_no_vars ctxt thm =
- str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
+fun string_of_thm_no_vars ctxt thm =
+ string_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
text {*
Theorem @{thm [source] conjI} is now printed as follows:
@{ML_response_fake [display, gray]
- "writeln (str_of_thm_no_vars @{context} @{thm conjI})"
+ "writeln (string_of_thm_no_vars @{context} @{thm conjI})"
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
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)
+ML{*fun string_of_thms ctxt thms =
+ commas (map (string_of_thm ctxt) thms)
-fun str_of_thms_no_vars ctxt thms =
- commas (map (str_of_thm_no_vars ctxt) thms) *}
+fun string_of_thms_no_vars ctxt thms =
+ commas (map (string_of_thm_no_vars ctxt) thms) *}
section {* Combinators\label{sec:combinators} *}
text {*
- (FIXME: Calling convention)
-
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
@@ -287,8 +285,8 @@
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 have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using
- the reverse application is much clearer than writing
+ if you have been exposed to Haskell's {\it 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*}
@@ -481,6 +479,7 @@
contains further information about combinators.
\end{readmore}
+ (FIXME: say something abou calling conventions)
*}
@@ -543,7 +542,7 @@
text {*
The function @{ML dest_ss in MetaSimplifier} returns a record containing all
information stored in the simpset, but we are only interested in the names of the
- simp-rules. So now you can feed in the current simpset into this function.
+ simp-rules. Now you can feed in the current simpset into this function.
The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
@{ML_response_fake [display,gray]
@@ -555,7 +554,7 @@
On the ML-level of Isabelle, you often have to work with qualified names;
these are strings with some additional information, such as positional information
- and qualifiers. Such bindings can be generated with the antiquotation
+ and qualifiers. Such qualified names can be generated with the antiquotation
@{text "@{binding \<dots>}"}.
@{ML_response [display,gray]
@@ -582,7 +581,8 @@
\end{isabelle}
(FIXME give a better example why bindings are important; maybe
- give a pointer to \isacommand{local\_setup})
+ give a pointer to \isacommand{local\_setup}; if not, then explain
+ why @{ML snd} is needed)
While antiquotations have many applications, they were originally introduced
in order to avoid explicit bindings of theorems such as:
@@ -605,7 +605,7 @@
text {*
One way to construct Isabelle terms, is by using the antiquotation
- \mbox{@{text "@{term \<dots>}"}}. For example:
+ \mbox{@{text "@{term \<dots>}"}}. For example
@{ML_response [display,gray]
"@{term \"(a::nat) + b = c\"}"
@@ -613,18 +613,67 @@
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
will show the term @{term "(a::nat) + b = c"}, but printed using the internal
- representation corresponding to the data type @{ML_type "term"}.
-
- This internal representation uses the usual de Bruijn index mechanism---where
- bound variables are represented by the constructor @{ML Bound}. The index in
+ representation corresponding to the datatype @{ML_type "term"}. Since Isabelle
+ uses Church-style terms, the datatype @{ML_type term} must be defined in
+ conjunction with types, that is the datatype @{ML_type typ}:
+*}
+
+ML_val{*datatype typ =
+ Type of string * typ list
+| TFree of string * sort
+| TVar of indexname * sort
+datatype term =
+ Const of string * typ
+| Free of string * typ
+| Var of indexname * typ
+| Bound of int
+| Abs of string * typ * term
+| $ of term * term *}
+
+text {*
+ The datatype for terms uses the usual de Bruijn index mechanism---where
+ bound variables are represented by the constructor @{ML Bound}.
+
+ @{ML_response_fake [display, gray]
+ "@{term \"\<lambda>x y. x y\"}"
+ "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
+
+ 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. Note that
the names of bound variables are kept at abstractions for printing purposes,
and so should be treated only as ``comments''. Application in Isabelle is
- realised with the term-constructor @{ML $}.
+ realised with the term-constructor @{ML $}.
+
+ Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free})
+ and variables (term-constructor @{ML Var}). The latter correspond to the schematic
+ variables that show up with a question mark in front of them. Consider the following
+ two examples
+
+ @{ML_response_fake [display, gray]
+"let
+ val v1 = Var ((\"x\", 3), @{typ bool})
+ val v2 = Var ((\"x1\",3), @{typ bool})
+in
+ writeln (Syntax.string_of_term @{context} v1);
+ writeln (Syntax.string_of_term @{context} v2)
+end"
+"?x3
+?x1.3"}
+
+ This is different from a free variable
+
+ @{ML_response_fake [display, gray]
+ "@{term \"x\"}"
+ "x"}
+
+ When constructing terms, you are usually concerned with free variables (for example
+ you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}).
+ If you deal with theorems, you have to observe the distinction. The same holds
+ for types.
\begin{readmore}
- Terms are described in detail in \isccite{sec:terms}. Their
+ Terms and types are described in detail in \isccite{sec:terms}. Their
definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
\end{readmore}
@@ -632,8 +681,8 @@
terms can be constructed. For example
@{ML_response_fake_both [display,gray]
- "@{term \"(x::nat) x\"}"
- "Type unification failed \<dots>"}
+ "@{term \"x x\"}"
+ "Type unification failed: Occurs check!"}
raises a typing error, while it perfectly ok to construct the term
@@ -689,7 +738,6 @@
\end{readmore}
*}
-
section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
text {*
@@ -865,7 +913,7 @@
@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
the name of the constant @{text "Nil"} depends on the theory in which the
- term constructor is defined (@{text "List"}) and also in which data type
+ 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
\mbox{@{text "(op *)"}}:
@@ -877,7 +925,7 @@
While you could use the complete name, for example
@{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
matching against @{text "Nil"}, this would make the code rather brittle.
- The reason is that the theory and the name of the data type can easily change.
+ The reason is that the theory and the name of the datatype can easily change.
To make the code more robust, it is better to use the antiquotation
@{text "@{const_name \<dots>}"}. With this antiquotation you can harness the
variable parts of the constant's name. Therefore a function for
@@ -918,11 +966,11 @@
*}
-ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
+ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
text {* This can be equally written with the combinator @{ML "-->"} as: *}
-ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
+ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
text {*
A handy function for manipulating terms is @{ML map_types}: it takes a
@@ -945,6 +993,8 @@
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
(FIXME: a readmore about types)
+
+ (Explain @{ML Term.add_tvarsT} and @{ML Term.add_tfreesT})
*}
@@ -1663,6 +1713,9 @@
text {* @{ML PureThy.add_thms_dynamic} *}
+local_setup {*
+ LocalTheory.note Thm.theoremK
+ ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
(* FIXME: some code below *)
@@ -1910,7 +1963,7 @@
"The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
To see the proper linebreaking, you can try out the function on a bigger term
- and type.
+ and type. For example:
@{ML_response_fake [display,gray]
"tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
@@ -1919,26 +1972,75 @@
*}
+ML {* pprint (Pretty.big_list "header" (map (Pretty.str o string_of_int) (4 upto 10))) *}
+
+text {*
+chunks inserts forced breaks (unlike blk where you have to do this yourself)
+*}
+
+ML {* (Pretty.chunks [Pretty.str "a", Pretty.str "b"],
+ Pretty.blk (0, [Pretty.str "a", Pretty.str "b"])) *}
+
+ML {*
+fun setmp_show_all_types f =
+ setmp show_all_types
+ (! show_types orelse ! show_sorts orelse ! show_all_types) f;
+
+val ctxt = @{context};
+val t1 = @{term "undefined::nat"};
+val t2 = @{term "Suc y"};
+val pty = Pretty.block (Pretty.breaks
+ [(setmp show_question_marks false o setmp_show_all_types)
+ (Syntax.pretty_term ctxt) t1,
+ Pretty.str "=", Syntax.pretty_term ctxt t2]);
+pty |> Pretty.string_of |> priority
+*}
+
+text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely *}
+
+
+ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> writeln *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+
+
+ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of |> writeln *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+
text {*
Still to be done:
- @{ML Pretty.big_list},
-
- @{ML Pretty.chunks}
-
- equations
-
- colours
-
What happens with big formulae?
\begin{readmore}
The general infrastructure for pretty-printing is implemented in the file
@{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
contains pretty-printing functions for terms, types, theorems and so on.
+
+ @{ML_file "Pure/General/markup.ML"}
\end{readmore}
*}
+text {*
+ printing into the goal buffer as part of the proof state
+*}
+
+
+ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> writeln *}
+ML {* (Pretty.str "bar") |> Pretty.string_of |> writeln *}
+
+text {* writing into the goal buffer *}
+
+ML {* fun my_hook interactive state =
+ (interactive ? Proof.goal_message (fn () => Pretty.str
+"foo")) state
+*}
+
+setup {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
+
+lemma "False"
+oops
+
+
section {* Misc (TBD) *}
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}