isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:4172c0743cf2
+:352e31d9dacc
 text {*
 The easiest way to get the string of a theorem is to transform it
 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"},
 @{text "?Q"} and so on. They are needed in order to able to
 instantiate theorems when they are applied. For example the theorem
 in
 thm'
 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:
 @{ML_response_fake [display, gray]
 sometimes necessary to do some ``plumbing'' in order to fit functions
 together. We have already seen such plumbing in the function @{ML
 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.
 @{ML_response_fake [display, gray]
 "let
 end"
 "m + n, m * n, m - n"}
 *}
 text {*
-In this example we obtain three terms where @{text m} and @{text n} are of
+In this example we obtain three terms in which @{text m} and @{text n} are of
-type @{typ "nat"}. However, if you have only a single term, then @{ML
+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}
 and @{ML check_terms in Syntax}.} For example
 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 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
+purpose is to print logical entities inside \LaTeX-documents. Document
-of the user level and therefore we are not interested in them in this
+antiquotations are part of the user level and therefore we are not
-Tutorial, except in Appendix \ref{rec:docantiquotations} where we show how
+interested in them in this Tutorial, except in Appendix
-to implement your own document antiquotations.}  For example, one can print
+\ref{rec:docantiquotations} where we show how to implement your own document
-out the name of the current theory by typing
+antiquotations.}  For example, one can print out the name of the current
+theory by typing
 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
 where @{text "@{theory}"} is an antiquotation that is substituted with the
 current theory (remember that we assumed we are inside the theory
 @{ML_ind  define in LocalTheory}.  This function is used below to define
 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
 *}
 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:
 \begin{isabelle}
 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"
+ML %linenosgray{*let
-(Args.context -- Scan.lift Args.name_source >>
+val parser = Args.context -- Scan.lift Args.name_source
-(fn (ctxt, s) =>
-s |> ProofContext.read_term_pattern ctxt
+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
+ProofContext} (Line 5); the next two lines transform the term into a string
-so that the ML-system can understand them. The function @{ML_ind atomic in
+so that the ML-system can understand them. An example for the usage
-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\")"}
 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) *}
+section {* Storing Data in Isabelle (TBD) *}
 text {*
-Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we
+Isabelle provides mechanisms to store (and retrieve) arbitrary data. Before we
-explain this mechanism, let us digress a bit. Convenitional wisdom is that the
+explain them, let us digress: Convenitional wisdom has it that
-type-system of ML ensures that for example an @{ML_type "'a list"} can only
+ML's type-system ensures that for example an @{ML_type "'a list"} can only
-hold elements of type @{ML_type "'a"}.
+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
-ML{*signature UNIVERSAL_TYPE =
+inject and project elements of different type into for example into a list.
-sig
+We will show this by storing an integer and boolean in a list. What is important
-type t
+that access to the data is done in a type-safe manner.
-val embed: unit -> ('a -> t) * (t -> 'a option)
+Let us first define projection and injection functions for booleans and integers.
+*}
+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{*structure U:> UNIVERSAL_TYPE =
+text {*
-struct
+We can now build a list injecting @{ML_text "13"} and @{ML_text "true"} as
-type t = exn
+its two elements.
+*}
-fun 'a embed () =
-let
+ML{* val list = [inject_int 13, inject_bool true]*}
-exception E of 'a
-fun project (e: t): 'a option =
+ML {*
-case e of
+project_int (nth list 0)
-E a => SOME a
+*}
-| _ => NONE
-in
+ML {*
-(E, project)
+project_bool (nth list 1)
-end
+*}
-end*}
+(**************************************************)
-text {*
+(* bak                                            *)
-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 (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! *}
 ML {* val my_thms = ref ([]: thm list) *}

changeset 325	352e31d9dacc
parent 324	4172c0743cf2
child 326	f76135c6c527