isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:ebbd0dd008c8
+:fee4942c4770
 chapter {* First Steps *}
 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 written in
+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{tabular}{@ {}l}
 \isacommand{theory} FirstSteps\\
 text {*
 The easiest and quickest way to include code in a theory is
-by using the \isacommand{ML}-command. For example\smallskip
+by using the \isacommand{ML}-command. For example:
 \begin{isabelle}
 \begin{graybox}
 \isacommand{ML}~@{text "\<verbopen>"}\isanewline
 \hspace{5mm}@{ML "3 + 4"}\isanewline
 @{text "\<verbclose>"}\isanewline
 @{text "> 7"}\smallskip
 \end{graybox}
 \end{isabelle}
-Like ``normal'' Isabelle proof scripts,
+Like normal Isabelle proof scripts,
 \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of
 your Isabelle environment. The code inside the \isacommand{ML}-command
 can also contain value and function bindings, and even those can be
 undone when the proof script is retracted. As mentioned earlier, we will
 drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
-whenever we show code.
+scaffolding whenever we show code.
 Once a portion of code is relatively stable, one usually wants to
 export it to a separate ML-file. Such files can then be included in a
-theory by using \isacommand{uses} in the header of the theory, like
+theory by using the \isacommand{uses}-command in the header of the theory, like:
 \begin{center}
 \begin{tabular}{@ {}l}
 \isacommand{theory} FirstSteps\\
 \isacommand{imports} Main\\
 The function @{ML "warning"} should only be used for testing purposes, because any
 output this function generates will be overwritten as soon as an error is
 raised. For printing anything more serious and elaborate, the
 function @{ML tracing} is more appropriate. This function writes all output into
-a separate tracing buffer. For example
+a separate tracing buffer. For example:
 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 It is also possible to redirect the ``channel'' where the string @{text "foo"} is
 printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive
 text {*
 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
 will cause that all tracing information is printed into the file @{text "foo.bar"}.
-Error messages can be printed using the function @{ML error}, as in
+You can print out error messages with the function @{ML error}, as in:
 @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
 *}
 @{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
-@{text FirstSteps}). The name of this theory can be extracted with
+@{text FirstSteps}). The name of this theory can be extracted using
 the function @{ML "Context.theory_name"}.
-Note, however, that antiquotations are statically scoped, that is their value is
+Note, however, that antiquotations are statically linked, that is their value is
 determined at ``compile-time'', not ``run-time''. For example the function
 *}
 ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 text {*
-does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a
+does \emph{not} return the name of the current theory, if it is run in a
 different theory. Instead, the code above defines the constant function
 that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
 function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is
 \emph{not} replaced with code that will look up the current theory in
 some data structure and return it. Instead, it is literally
 or simpsets:
 @{ML_response_fake [display,gray]
 "let
-val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
+val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset}
 in
 map #name (Net.entries rules)
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
-The code about simpsets extracts the theorem names that are stored in the
+The code about simpsets extracts the theorem names stored in the
 current simpset.  We get hold of the current simpset with the antiquotation
 @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
 containing all information about the simpset. The rules of a simpset are
 stored in a \emph{discrimination net} (a datastructure for fast
 indexing). From this net we can extract the entries using the function @{ML
 and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
 in @{ML_file "Pure/net.ML"}.
 \end{readmore}
 While antiquotations have many applications, they were originally introduced in order
-to avoid explicit bindings for theorems such as
+to avoid explicit bindings for theorems such as:
 *}
 ML{*val allI = thm "allI" *}
 text {*
 These bindings are difficult to maintain and also can be accidentally
-overwritten by the user. This often breakes definitional
+overwritten by the user. This often breakes Isabelle
 packages. Antiquotations solve this problem, since they are ``linked''
-statically at compile-time. However, this static linkage also limits their
+statically at compile-time.  However, this static linkage also limits their
-usefulness in cases where data needs to be build up dynamically. In the course of
+usefulness in cases where data needs to be build up dynamically. In the
-this introduction, we will learn more about
+course of this introduction, we will learn more about these antiquotations:
-these antiquotations: they greatly simplify Isabelle programming since one
+they greatly simplify Isabelle programming since one can directly access all
-can directly access all kinds of logical elements from ML.
+kinds of logical elements from th ML-level.
 *}
 section {* Terms and Types *}
 text {*
 One way to construct terms of Isabelle on the ML-level 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>"}
 from what you see at the user level, because the layers of
 parsing/type-checking/pretty printing can be quite elaborate.
 \begin{exercise}
 Look at the internal term representation of the following terms, and
-find out why they are represented like this.
+find out why they are represented like this:
 \begin{itemize}
 \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}
 \item @{term "\<lambda>(x,y). P y x"}
 \item @{term "{ [x::int] | x. x \<le> -2 }"}
 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 where it is not (since it is already constructed by a meta-implication).
-Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
+Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:
 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 \begin{readmore}
 Types are described in detail in \isccite{sec:types}. Their
 text {*
 While antiquotations are very convenient for constructing terms, they can
 only construct fixed terms (remember they are ``linked'' at
 compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external}
-for a function that pattern-matches over terms and where the pattern are
+for a function that pattern-matches over terms and where the patterns are
-constructed from antiquotations.  However, one often needs to construct
+constructed using antiquotations.  However, one often needs to construct
 terms dynamically. For example, a function that returns the implication
 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term
-"\<tau>"} as arguments can only be written as
+"\<tau>"} as arguments can only be written as:
 *}
 ML{*fun make_imp P Q tau =
 let
 val x = Free ("x",tau)
 in
 Logic.all x (Logic.mk_implies (P $ x, Q $ x))
 end *}
 text {*
 The reason is that one cannot pass the arguments @{term P}, @{term Q} and
 @{term "tau"} into an antiquotation. For example the following does \emph{not} work:
 *}
 ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 text {*
 \begin{readmore}
-There are many functions in @{ML_file "Pure/logic.ML"} and
+There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
 @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms
 and types easier.\end{readmore}
 Have a look at these files and try to solve the following two exercises:
 Write a function which takes two terms representing natural numbers
 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
 number representing their sum.
 \end{exercise}
+(FIXME: maybe should go)
-(FIXME: operation from page 19 of the implementation manual)
+*}
+ML{*fun nat_to_int t =
+(case t of
+@{typ nat} => @{typ int}
+| Type (s, ts) => Type (s, map nat_to_int ts)
+| _ => t)*}
+text {*
+@{ML_response_fake [display,gray]
+"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\")"}
 *}
 section {* Type-Checking *}
 text {*
 \begin{exercise}
 Check that the function defined in Exercise~\ref{fun:revsum} returns a
 result that type-checks.
 \end{exercise}
-(FIXME: @{text "ctyp_of"})
+(FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
 *}
 section {* Theorems *}
 *}
 ML{*val double =
 (fn x => (x, x))
 #-> (fn x => fn y => x + y)*}
+text {*
-text {*
 (FIXME: find a good exercise for combinators)
 *}
+(*<*)
+setup {*
+Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)]
+*}
+lemma "bar = (1::nat)"
+oops
+setup {*
+Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)]
+#> PureThy.add_defs false [((Binding.name "foo_def",
+Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])]
+#> snd
+*}
+lemma "foo = (1::nat)"
+apply(simp add: foo_def)
+done
+thm foo_def
+(*>*)
 end

changeset 89	fee4942c4770
parent 87	90189a97b3f8
child 92	4e3f262a459d