# HG changeset patch # User Christian Urban # Date 1254093687 -7200 # Node ID 92f6a772e013417e0482a7b2d4c934909644d609 # Parent 2b7c08d90e2ef90c29d78927952da189407f932e some polishing diff -r 2b7c08d90e2e -r 92f6a772e013 ProgTutorial/FirstSteps.thy --- 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 \}"} 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 \ 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! *} diff -r 2b7c08d90e2e -r 92f6a772e013 ProgTutorial/General.thy --- 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} *} diff -r 2b7c08d90e2e -r 92f6a772e013 ProgTutorial/Package/Ind_Code.thy --- 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 = diff -r 2b7c08d90e2e -r 92f6a772e013 progtutorial.pdf Binary file progtutorial.pdf has changed