isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:a0edabf14457
+:3d4b49921cdb
 chapter {* First Steps *}
 text {*
-Isabelle programming is done in Standard ML.
+Isabelle programming is done in SML.  Just like lemmas and proofs, SML-code
-Just like lemmas and proofs, SML-code in Isabelle is part of a
+in Isabelle is part of a theory. If you want to follow the code written in
-theory. If you want to follow the code written in this chapter, we
+this chapter, we assume you are working inside the theory defined by
-assume you are working inside the theory defined by
 \begin{center}
 \begin{tabular}{@ {}l}
 \isacommand{theory} FirstSteps\\
 \isacommand{imports} Main\\
 section {* Debugging and Printing *}
 text {*
-During developments you might find it necessary to quickly inspect some data
+During development you might find it necessary to inspect some data
 in your code. This can be done in a ``quick-and-dirty'' fashion using
 the function @{ML "warning"}. For example
 @{ML [display] "warning \"any string\""}
-will print out @{ML_text [quotes] "any string"} inside the response buffer of Isabelle.
+will print out @{ML_text [quotes] "any string"} inside the response buffer
-If you develop under PolyML, then there is a convenient, though again
+of Isabelle.  This function expects a string. If you develop under PolyML,
-``quick-and-dirty'', method for converting values into strings,
+then there is a convenient, though again ``quick-and-dirty'', method for
-for example:
+converting values into strings, for example:
 @{ML [display] "warning (makestring 1)"}
 However this only works if the type of what is converted is monomorphic and is not
 a function.
 The funtion @{ML "warning"} should only be used for testing purposes, because any
 output this funtion generates will be overwritten as soon as an error is
-raised. Therefore for printing anything more serious and elaborate, the
+raised. For printing anything more serious and elaborate, the
 function @{ML tracing} should be used. This function writes all output into
 a separate tracing buffer. For example
 @{ML [display] "tracing \"foo\""}
-It is also possible to redirect the channel where the @{ML_text "foo"} is
+It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is
 printed to a separate file, e.g. to prevent Proof General from choking on massive
 amounts of trace output. This rediretion can be achieved using the code
 *}
 ML{*
 In a similar way you can use antiquotations to refer to theorems or simpsets:
 @{ML [display] "@{thm allI}"}
 @{ML [display] "@{simpset}"}
-While antiquotations nowadays have many applications, they were originally introduced to
+While antiquotations have many applications, they were originally introduced to
 avoid explicit bindings for theorems such as
 *}
 ML {*
 val allI = thm "allI"
 text {*
 These bindings were difficult to maintain and also could be accidentally
 overwritten by the user. This usually broke definitional
 packages. Antiquotations solve this problem, since they are ``linked''
-statically at compile-time. However, that also sometimes limits there
+statically at compile-time. However, that also sometimes limits their
 applicability. In the course of this introduction, we will learn more about
 these antiquotations: they greatly simplify Isabelle programming since one
 can directly access all kinds of logical elements from ML.
 *}
 \mbox{@{text "@{term \<dots>}"}}. For example
 @{ML_response [display] "@{term \"(a::nat) + b = c\"}"
 "Const (\"op =\", \<dots>)  $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
-This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
+This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
 representation of this term. This internal representation corresponds to the
 datatype @{ML_type "term"}.
 The internal representation of terms uses the usual de Bruijn index mechanism where bound
 variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
 \end{exercise}
 @{ML [display] "print_depth 50"}
 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
-inserting the invisible @{text "Trueprop"} coercions whenever necessary.
+inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
 Consider for example
 @{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)"}
 @{ML_response [display] "@{prop \"P x\"}"
 "Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>))"}
 which inserts the coercion in the latter case and
 @{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
 @{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
-which does not.
+which does not (since it is already constructed using the meta-implication).
 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
 @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 text {*
 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
 to both functions.
 One tricky point in constructing terms by hand is to obtain the
-fully qualified name for constants. For example the names for @{text "zero"} or
+fully qualified name for constants. For example the names for @{text "zero"} and
 @{text "+"} are more complex than one first expects, namely
 \begin{center}
 @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}.
 \end{center}
 @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
-Similarly, types can be constructed for example as follows:
+Similarly, types can be constructed manually, for example as follows:
 *}
 ML {*
 fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2])
 text {*
 We can freely construct and manipulate terms, since they are just
 arbitrary unchecked trees. However, we eventually want to see if a
 term is well-formed, or type checks, relative to a theory.
-Type-checking is done via the function @{ML cterm_of}, which turns
+Type-checking is done via the function @{ML cterm_of}, which converts
 a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term.
 Unlike @{ML_type term}s, which are just trees, @{ML_type
 "cterm"}s are abstract objects that are guaranteed to be
-type-correct, and that can only be constructed via the official
+type-correct, and that can only be constructed via the ``official
-interfaces.
+interfaces''.
-Type checking is always relative to a theory context. For now we can use
+Type checking is always relative to a theory context. For now we use
 the @{ML "@{theory}"} antiquotation to get hold of the current theory.
 For example we can write
 @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
 $ zero $ zero)
 end" "0 + 0"}
 \begin{exercise}
 Check that the function defined in Exercise~\ref{fun:revsum} returns a
-result that type checks.
+result that type-checks.
 \end{exercise}
 *}
 section {* Theorems *}
 text {*
-Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are
+Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
-abstract objects that can only be built by going through the kernel
+that can only be built by going through interfaces, which means that all your proofs
-interfaces, which means that all your proofs will be checked.
+will be checked.
 To see theorems in ``action'', let us give a proof for the following statement
 *}
 lemma
 }
 \]
 \begin{readmore}
-For how the functions @{text "assume"}, @{text "forall_elim"} etc work
+For the functions @{text "assume"}, @{text "forall_elim"} etc
 see \isccite{sec:thms}. The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}.
 \end{readmore}
 *}
 where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open
 subgoals.
 Since the goal @{term C} can potentially be an implication, there is a
 @{text "#"} wrapped around it, which prevents that premises are
-misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
+misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
 prop"} is just the identity function and used as a syntactic marker.
 \begin{readmore}
 For more on goals see \isccite{sec:tactical-goals}.
 \end{readmore}
 \begin{readmore}
 See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
 sequences. However in day-to-day Isabelle programming, one rarely
 constructs sequences explicitly, but uses the predefined tactic
-combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}).
+combinators (tacticals) instead. See @{ML_file "Pure/tctical.ML"}
-(FIXME: Pointer to the old reference manual)
+for the code; see Chapters 3 and 4 in the old Isabelle Reference Manual.
 \end{readmore}
 While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they
 are expected to leave the conclusion @{term C} intact, with the
 exception of possibly instantiating schematic variables.
 To see how tactics work, let us transcribe a simple @{text apply}-style
-proof from the tutorial~\cite{isa-tutorial} into ML:
+proof into ML:
 *}
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 apply (erule disjE)
 apply (rule disjI2)
 To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt xs As C tac"} sets
 up a goal state for proving the goal @{text C} under the assumptions @{text As}
 (empty in the proof at hand)
 with the variables @{text xs} that will be generalised once the
 goal is proved. The @{text "tac"} is the tactic which proves the goal and which
-can make use of the local assumptions.
+can make use of the local assumptions (there are none in this example).
 @{ML_response_fake [display]
 "let
 val ctxt = @{context}
 val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

changeset 50	3d4b49921cdb
parent 49	a0edabf14457
child 52	a04bdee4fb1e