--- a/ProgTutorial/FirstSteps.thy Mon Sep 28 23:52:06 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Tue Sep 29 22:10:48 2009 +0200
@@ -266,10 +266,8 @@
into a @{ML_type term} using the function @{ML_ind prop_of}.
*}
-ML {* Thm.rep_thm @{thm mp} *}
-
ML{*fun string_of_thm ctxt thm =
- Syntax.string_of_term ctxt (prop_of thm)*}
+ string_of_term ctxt (prop_of thm)*}
text {*
Theorems also include schematic variables, such as @{text "?P"},
@@ -296,7 +294,7 @@
end
fun string_of_thm_no_vars ctxt thm =
- Syntax.string_of_term ctxt (prop_of (no_vars ctxt thm))*}
+ string_of_term ctxt (prop_of (no_vars ctxt thm))*}
text {*
Theorem @{thm [source] conjI} is now printed as follows:
@@ -638,7 +636,7 @@
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
plumbing is also needed in situations where a functions operate over lists,
- but one calculates only with a single entity. An example is the function
+ but one calculates only with a single element. An example is the function
@{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
of terms.
@@ -655,8 +653,8 @@
*}
text {*
- In this example we obtain three terms where @{text m} and @{text n} are of
- type @{typ "nat"}. However, if you have only a single term, then @{ML
+ In this example we obtain three terms in which @{text m} and @{text n} are of
+ type @{typ "nat"}. If you have only a single term, then @{ML
check_terms in Syntax} needs plumbing. This can be done with the function
@{ML singleton}.\footnote{There is already a function @{ML check_term in
Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
@@ -692,18 +690,20 @@
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 ML-antiquotations, often just called
+ is realised in Isabelle with ML-antiquotations, often just called
antiquotations.\footnote{There are two kinds of antiquotations in Isabelle,
- which have very different purpose and infrastructures. The first kind,
+ which have very different purposes 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
+ purpose is to print logical entities inside \LaTeX-documents. Document
+ antiquotations 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
+
@{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
@@ -786,9 +786,9 @@
*}
local_setup %gray {*
- snd o LocalTheory.define Thm.internalK
+ LocalTheory.define Thm.internalK
((@{binding "TrueConj"}, NoSyn),
- (Attrib.empty_binding, @{term "True \<and> True"})) *}
+ (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
text {*
Now querying the definition you obtain:
@@ -813,19 +813,22 @@
as follows.
*}
-ML %linenosgray{*ML_Antiquote.inline "term_pat"
- (Args.context -- Scan.lift Args.name_source >>
- (fn (ctxt, s) =>
- s |> ProofContext.read_term_pattern ctxt
+ML %linenosgray{*let
+ val parser = Args.context -- Scan.lift Args.name_source
+
+ fun term_pat (ctxt, str) =
+ str |> ProofContext.read_term_pattern ctxt
|> ML_Syntax.print_term
- |> ML_Syntax.atomic))*}
+ |> ML_Syntax.atomic
+in
+ ML_Antiquote.inline "term_pat" (parser >> term_pat)
+end*}
text {*
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 transform the term into a string
- so that the ML-system can understand them. The function @{ML_ind atomic in
- ML_Syntax} just encloses the term in parentheses. An example for the usage
+ ProofContext} (Line 5); the next two lines transform the term into a string
+ so that the ML-system can understand them. An example for the usage
of this antiquotation is:
@{ML_response_fake [display,gray]
@@ -841,81 +844,50 @@
\end{readmore}
*}
-section {* Storing Data (TBD) *}
-
-text {*
- Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we
- explain this mechanism, let us digress a bit. Convenitional wisdom is that the
- type-system of ML ensures that for example an @{ML_type "'a list"} can only
- hold elements of type @{ML_type "'a"}.
-*}
-
-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*}
+section {* Storing Data in Isabelle (TBD) *}
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.
+ Isabelle provides mechanisms to store (and retrieve) arbitrary data. Before we
+ explain them, let us digress: Convenitional wisdom has it that
+ ML's type-system ensures that for example an @{ML_type "'a list"} can only
+ hold elements of the same type, namely @{ML_type "'a"}. Still, by some arguably
+ accidental features of ML, one can implement a universal type. In Isabelle it
+ is implemented as @{ML_type Universal.universal}. This type allows one to
+ inject and project elements of different type into for example into a list.
+ We will show this by storing an integer and boolean in a list. What is important
+ that access to the data is done in a type-safe manner.
- in library.ML
+ Let us first define projection and injection functions for booleans and integers.
*}
-ML_val{*structure Object = struct type T = exn end; *}
+ML{*local
+ val fn_int = Universal.tag () : int Universal.tag
+ val fn_bool = Universal.tag () : bool Universal.tag
+in
+ val inject_int = Universal.tagInject fn_int;
+ val inject_bool = Universal.tagInject fn_bool;
+ val project_int = Universal.tagProject fn_int;
+ val project_bool = Universal.tagProject fn_bool
+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 (implode [s1, " ", s2, " ", s3, "\n"])
- end*}
+text {*
+ We can now build a list injecting @{ML_text "13"} and @{ML_text "true"} as
+ its two elements.
+*}
+
+ML{* val list = [inject_int 13, inject_bool true]*}
-ML_val{*structure t = Test(U) *}
-
-ML_val{*structure Datatab = Table(type key = int val ord = int_ord);*}
+ML {*
+ project_int (nth list 0)
+*}
-ML {* LocalTheory.restore *}
-ML {* LocalTheory.set_group *}
+ML {*
+ project_bool (nth list 1)
+*}
-
+(**************************************************)
+(* bak *)
+(**************************************************)
(*
section {* Do Not Try This At Home! *}