isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:5c211dd7e5ad
+:ab9e09076462
 text {*
 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
 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.
 *}
 Once a portion of code is relatively stable, you usually want to export it
 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\\
 \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\
 \isacommand{begin}\\
 \ldots\\
 \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\\
 \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
 \isacommand{begin}\\
 \ldots
 \end{tabular}
-\end{center}
+\end{quote}
 Note that no parentheses are given this time.
 *}
 section {* Debugging and Printing\label{sec:printing} *}
 "\"1\""}
 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 {*
 In this example the function @{ML term_of} extracts the @{ML_type term} from
 a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be
 printed, you can use the function @{ML commas} to separate them.
 *}
-ML{*fun str_of_cterms ctxt ts =
+ML{*fun string_of_cterms ctxt ts =
-commas (map (str_of_cterm 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 =
+ML{*fun string_of_thm ctxt thm =
-str_of_cterm ctxt (#prop (crep_thm 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
 these schematic variables into free variables using the
 function @{ML Variable.import_thms}.
 val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
 in
 thm'
 end
-fun str_of_thm_no_vars ctxt thm =
+fun string_of_thm_no_vars ctxt thm =
-str_of_cterm ctxt (#prop (crep_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 =
+ML{*fun string_of_thms ctxt thms =
-commas (map (str_of_thm ctxt) thms)
+commas (map (string_of_thm ctxt) thms)
-fun str_of_thms_no_vars ctxt thms =
+fun string_of_thms_no_vars ctxt thms =
-commas (map (str_of_thm_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
 actually ease the understanding and also the programming.
 the first component of the pair (Line 4) and finally incrementing the first
 component by 4 (Line 5). This kind of cascading manipulations of values is quite
 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
+if you have been exposed to Haskell's {\it do}-notation. Writing the function
-the reverse application is much clearer than writing
+@{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*}
 text {* or *}
 "Pure/library.ML"}
 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
 contains further information about combinators.
 \end{readmore}
+(FIXME: say something abou calling conventions)
 *}
 section {* Antiquotations *}
 end*}
 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]
 "get_thm_names_from_ss @{simpset}"
 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 Again, this way of referencing simpsets makes you independent from additions
 of lemmas to the simpset by the user that potentially cause loops.
 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]
 "@{binding \"name\"}"
 "name"}
 \isacommand{thm}~@{text "TrueConj_def"}\\
 @{text "> "}~@{thm TrueConj_def}
 \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:
 *}
 section {* Terms and Types *}
 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\"}"
 "Const (\"op =\", \<dots>) $
 (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"}.
+representation corresponding to the datatype @{ML_type "term"}. Since Isabelle
+uses Church-style terms, the datatype @{ML_type term} must be defined in
-This internal representation uses the usual de Bruijn index mechanism---where
+conjunction with types, that is the datatype @{ML_type typ}:
-bound variables are represented by the constructor @{ML Bound}.  The index in
+*}
+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 $}.
+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}
 Constructing terms via antiquotations has the advantage that only typable
 terms can be constructed. For example
 @{ML_response_fake_both [display,gray]
-"@{term \"(x::nat) x\"}"
+"@{term \"x x\"}"
-"Type unification failed \<dots>"}
+"Type unification failed: Occurs check!"}
 raises a typing error, while it perfectly ok to construct the term
 @{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"}
 Types are described in detail in \isccite{sec:types}. Their
 definition and many useful operations are implemented
 in @{ML_file "Pure/type.ML"}.
 \end{readmore}
 *}
 section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
 text {*
 While antiquotations are very convenient for constructing terms, they can
 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
 @{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 *)"}}:
 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
 Const (\"HOL.times_class.times\", \<dots>))"}
 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
 matching against constants that have a polymorphic type should
 be written as follows.
 when defining constants. For example the function returning a function
 type is as follows:
 *}
-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
 function and applies it to every type in a term. You can, for example,
 change every @{typ nat} in a term into an @{typ int} using the function:
 "map_types nat_to_int @{term \"a = (1::nat)\"}"
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
 (FIXME: a readmore about types)
+(Explain @{ML Term.add_tvarsT} and @{ML Term.add_tfreesT})
 *}
 section {* Type-Checking *}
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 text {* @{ML PureThy.add_thms_dynamic} *}
+local_setup {*
+LocalTheory.note Thm.theoremK
+((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
 (* FIXME: some code below *)
 (*<*)
 @{ML_response_fake [display,gray]
 "tell_type @{context} @{term \"min (Suc 0)\"}"
 "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 =))))\"}"
 "The term \"op = (op = (op = (op = (op = op =))))\" has type
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 *}
+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"*}
 end

changeset 250	ab9e09076462
parent 249	5c211dd7e5ad
child 251	cccb25ee1309