--- a/ProgTutorial/FirstSteps.thy Tue Aug 25 00:07:37 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Mon Sep 28 01:21:27 2009 +0200
@@ -6,6 +6,17 @@
chapter {* First Steps *}
text {*
+ \begin{flushright}
+ {\em
+ ``We will most likely never realize the full importance of painting the Tower,\\
+ that it is the essential element in the conservation of metal works and the\\
+ more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex]
+ Gustave Eiffel, In The 300-Meter Tower.\footnote{The Eiffel Tower has been
+ re-painted 18 times since its initial construction, an average of once every
+ seven years. It takes more than a year for a team of 25 painters to paint the Tower
+ from top to bottom.}\\[1ex]
+ \end{flushright}
+
Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
Isabelle must be 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
@@ -672,13 +683,23 @@
*}
-section {* Antiquotations *}
+section {* ML-Antiquotations *}
text {*
The main advantage of embedding all code in a theory is that the code can
contain references to entities defined on the logical level of Isabelle. By
- this we mean definitions, theorems, terms and so on. This kind of reference is
- realised with antiquotations, sometimes also referred to as ML-antiquotations.
+ this we mean definitions, theorems, terms and so on. This kind of reference
+ is realised with ML-antiquotations, often also referred to as just
+ antiquotations.\footnote{There are two kinds of antiquotations in Isabelle,
+ which have very different purpose and infrastructures. The first kind,
+ described in this section, are \emph{ML-antiquotations}. They are used to
+ refer to entities (like terms, types etc) from Isabelle's logic layer inside
+ ML-code. The other kind of antiquotations are \emph{document} antiquotations. They
+ are used only in the text parts of Isabelle and their purpose is to print
+ logical entities inside \LaTeX-documents. They are part of the user level
+ and therefore we are not interested in them in this Tutorial, except in
+ Appendix \ref{rec:docantiquotations} where we show how to implement your own
+ document antiquotations.}
For example, one can print out the name of the current
theory by typing
@@ -782,12 +803,13 @@
It is also possible to define your own antiquotations. But you should
exercise care when introducing new ones, as they can also make your code
- also difficult to read. In the next section we will see how the (build in)
+ also difficult to read. In the next chapter we will see how the (build in)
antiquotation @{text "@{term \<dots>}"} can be used to construct terms. A
restriction of this antiquotation is that it does not allow you to use
schematic variables. If you want to have an antiquotation that does not have
- this restriction, you can implement your own using the function @{ML_ind
- ML_Antiquote.inline}. The code is as follows.
+ this restriction, you can implement your own using the function @{ML_ind
+ ML_Antiquote.inline}. The code for the antiquotation @{text "term_pat"} is
+ as follows.
*}
ML %linenosgray{*ML_Antiquote.inline "term_pat"
@@ -801,35 +823,96 @@
The parser in Line 2 provides us with a context and a string; this string is
transformed into a term using the function @{ML_ind read_term_pattern in
ProofContext} (Line 4); the next two lines print the term so that the
- ML-system can understand them. An example of this antiquotation is as
- follows.
+ ML-system can understand them. The function @{ML atomic in ML_Syntax}
+ just encloses the term in parentheses. An example for the usage of this
+ antiquotation is:
@{ML_response_fake [display,gray]
"@{term_pat \"Suc (?x::nat)\"}"
"Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
- which is the internal representation of the term @{text "Suc ?x"}.
+ which shows the internal representation of the term @{text "Suc ?x"}.
\begin{readmore}
The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
- for most antiquotations.
+ for most antiquotations. Most of the basic operations on ML-syntax are implemented
+ in @{ML_file "Pure/ML/ml_syntax.ML"}.
\end{readmore}
+*}
+
+section {* Storing Data (TBD) *}
+
+text {*
+ Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we
+ explain this mechanism.
+*}
+
+ML{*signature UNIVERSAL_TYPE =
+sig
+ type t
+
+ val embed: unit -> ('a -> t) * (t -> 'a option)
+end*}
+
+ML{*structure U:> UNIVERSAL_TYPE =
+ struct
+ type t = exn
+
+ fun 'a embed () =
+ let
+ exception E of 'a
+ fun project (e: t): 'a option =
+ case e of
+ E a => SOME a
+ | _ => NONE
+ in
+ (E, project)
+ end
+ end*}
- Note one source of possible confusion about antiquotations. There are two kinds
- of them in Isabelle, which have very different purpose and infrastructures. The
- first kind, described in this section, are \emph{ML-antiquotations}. They are
- used to refer to entities (like terms, types etc) from Isabelle's logic layer
- inside ML-code. They are ``linked'' statically at compile-time, which limits
- sometimes their usefulness in cases where, for example, terms needs to be
- built up dynamically.
+text {*
+ The idea is that type t is the universal type and that each call to embed
+ returns a new pair of functions (inject, project), where inject embeds a
+ value into the universal type and project extracts the value from the
+ universal type. A pair (inject, project) returned by embed works together in
+ that project u will return SOME v if and only if u was created by inject
+ v. If u was created by a different function inject', then project returns
+ NONE.
+
+ in library.ML
+*}
+
+ML_val{*structure Object = struct type T = exn end; *}
- The other kind of antiquotations are \emph{document} antiquotations.
- They are used only in the text parts of Isabelle and their purpose is to print
- logical entities inside \LaTeX-documents. They are part of the user level and
- therefore we are not interested in them in this Tutorial, except in
- Appendix \ref{rec:docantiquotations} where we show how to implement your
- own document antiquotations.
-*}
+ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
+ struct
+ val (intIn: int -> U.t, intOut) = U.embed ()
+ val r: U.t ref = ref (intIn 13)
+ val s1 =
+ case intOut (!r) of
+ NONE => "NONE"
+ | SOME i => Int.toString i
+ val (realIn: real -> U.t, realOut) = U.embed ()
+ val _ = r := realIn 13.0
+ val s2 =
+ case intOut (!r) of
+ NONE => "NONE"
+ | SOME i => Int.toString i
+ val s3 =
+ case realOut (!r) of
+ NONE => "NONE"
+ | SOME x => Real.toString x
+ val _ = tracing (implode [s1, " ", s2, " ", s3, "\n"])
+ end*}
+
+ML_val{*structure t = Test(U) *}
+
+ML_val{*structure Datatab = Table(type key = int val ord = int_ord);*}
+
+ML {* LocalTheory.restore *}
+ML {* LocalTheory.set_group *}
+
+
(*
section {* Do Not Try This At Home! *}
--- a/ProgTutorial/General.thy Tue Aug 25 00:07:37 2009 +0200
+++ b/ProgTutorial/General.thy Mon Sep 28 01:21:27 2009 +0200
@@ -2,7 +2,7 @@
imports Base FirstSteps
begin
-chapter {* General Infrastructure *}
+chapter {* Isabelle -- The Good, the Bad and the Ugly *}
text {*
Isabelle is build around a few central ideas. One is the LCF-approach to
@@ -1244,73 +1244,6 @@
valid local theory.
*}
-(*
-ML{*signature UNIVERSAL_TYPE =
-sig
- type t
-
- val embed: unit -> ('a -> t) * (t -> 'a option)
-end*}
-
-ML{*structure U:> UNIVERSAL_TYPE =
- struct
- type t = exn
-
- fun 'a embed () =
- let
- exception E of 'a
- fun project (e: t): 'a option =
- case e of
- E a => SOME a
- | _ => NONE
- in
- (E, project)
- end
- end*}
-
-text {*
- The idea is that type t is the universal type and that each call to embed
- returns a new pair of functions (inject, project), where inject embeds a
- value into the universal type and project extracts the value from the
- universal type. A pair (inject, project) returned by embed works together in
- that project u will return SOME v if and only if u was created by inject
- v. If u was created by a different function inject', then project returns
- NONE.
-
- in library.ML
-*}
-
-ML_val{*structure Object = struct type T = exn end; *}
-
-ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
- struct
- val (intIn: int -> U.t, intOut) = U.embed ()
- val r: U.t ref = ref (intIn 13)
- val s1 =
- case intOut (!r) of
- NONE => "NONE"
- | SOME i => Int.toString i
- val (realIn: real -> U.t, realOut) = U.embed ()
- val () = r := realIn 13.0
- val s2 =
- case intOut (!r) of
- NONE => "NONE"
- | SOME i => Int.toString i
- val s3 =
- case realOut (!r) of
- NONE => "NONE"
- | SOME x => Real.toString x
- val () = tracing (concat [s1, " ", s2, " ", s3, "\n"])
- end*}
-
-ML_val{*structure t = Test(U) *}
-
-ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
-
-ML {* LocalTheory.restore *}
-ML {* LocalTheory.set_group *}
-*)
-
section {* Storing Theorems\label{sec:storing} (TBD) *}
text {* @{ML_ind add_thms_dynamic in PureThy} *}
--- a/ProgTutorial/Package/Ind_Code.thy Tue Aug 25 00:07:37 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy Mon Sep 28 01:21:27 2009 +0200
@@ -239,12 +239,14 @@
*}
ML{*fun inst_spec ctrm =
- Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
+ Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm]
+ @{thm spec}*}
text {*
- This helper function instantiates the @{text "?x"} in the theorem
- @{thm spec} with a given @{ML_type cterm}. We call this helper function
- in the following tactic.\label{fun:instspectac}.
+ This helper function uses the function @{ML_ind instantiate' in Drule}
+ and instantiates the @{text "?x"} in the theorem @{thm spec} with a given
+ @{ML_type cterm}. We call this helper function in the following
+ tactic.\label{fun:instspectac}.
*}
ML{*fun inst_spec_tac ctrms =
Binary file progtutorial.pdf has changed