isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:609f9ef73494
+:a0edabf14457
 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\smallskip
 \isa{\isacommand{ML}
 \isacharverbatimopen\isanewline
 \hspace{5mm}@{ML "3 + 4"}\isanewline
 \isacharverbatimclose\isanewline
 @{ML_text "> 7"}\smallskip}
-Expressions inside \isacommand{ML} commands are immediately evaluated,
+Expressions inside \isacommand{ML}-commands are immediately evaluated,
 like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of
-your Isabelle environment. The code inside the \isacommand{ML} command
+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. From now on we will drop the
+undone when the proof script is retracted. In what follows we will drop the
 \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
 we show code and its response.
 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
 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
+output this funtion generates will be overwritten as soon as an error is
 raised. Therefore for printing anything more serious and elaborate, the
 function @{ML tracing} should be used. This function writes all output into
-a separate tracing buffer.
+a separate tracing buffer. For example
 @{ML [display] "tracing \"foo\""}
 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
 section {* Antiquotations *}
 text {*
-The main advantage of embedding all code
+The main advantage of embedding all code in a theory is that the code can
-in a theory is that the code can contain references to entities defined
+contain references to entities defined on the logical level of Isabelle (by
-on the logical level of Isabelle. This is done using antiquotations.
+this we mean definitions, theorems, terms and so on). This is done using
-For example, one can print out the name of
+antiquotations.  For example, one can print out the name of the current
-the current theory by typing
+theory by typing
 @{ML_response [display] "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 CookBook).
+current theory (remember that we assumed we are inside the theory
-The name of this theory can be extracted using the function
+@{ML_text FirstSteps}). The name of this theory can be extracted using
-@{ML "Context.theory_name"}.
+the function @{ML "Context.theory_name"}.
 Note, however, that antiquotations are statically scoped, that is the value is
 determined at ``compile-time'', not ``run-time''. For example the function
 *}
 In a similar way you can use antiquotations to refer to theorems or simpsets:
 @{ML [display] "@{thm allI}"}
 @{ML [display] "@{simpset}"}
-While antiquotations have many applications, they were originally introduced to
+While antiquotations nowadays 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
+These bindings were difficult to maintain and also could be accidentally
-by the user. This usually broke definitional packages. Antiquotations solve this
+overwritten by the user. This usually broke definitional
-problem, since they are ``linked'' statically at compile time.  In the course of this
+packages. Antiquotations solve this problem, since they are ``linked''
-introduction, we will learn more about these antiquotations: they greatly simplify
+statically at compile-time. However, that also sometimes limits there
-Isabelle programming since one can directly access all kinds of logical elements
+applicability. In the course of this introduction, we will learn more about
-from ML.
+these antiquotations: they greatly simplify Isabelle programming since one
+can directly access all kinds of logical elements from ML.
 *}
 section {* Terms and Types *}
 text {*
-One way to construct terms of Isabelle on the ML level is by using the antiquotation
+One way to construct terms of Isabelle on the ML-level is by using the antiquotation
-\mbox{@{text "@{term \<dots>}"}}:
+\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
 The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because
 these constants are defined within type classes; the prefix @{text "HOL"} indicates in
 which theory they are defined. Guessing such internal names can sometimes be quite hard.
 Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the
 expansion automatically, for example:
-*}
+@{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
-text {*
 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
-(FIXME: how to construct types manually)
+Similarly, types can be constructed for example as follows:
+*}
+ML {*
+fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2])
+*}
+text {*
+which can be equally written as
+*}
+ML {*
+fun make_fun_type tau1 tau2 = tau1 --> tau2
+*}
+text {*
 \begin{readmore}
 There are many functions in @{ML_file "Pure/logic.ML"} and
 @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms
-easier.\end{readmore}
+and types easier.\end{readmore}
 Have a look at these files and try to solve the following two exercises:
 *}
 number representing their sum.
 \end{exercise}
 *}
-section {* Type Checking *}
+section {* Type-Checking *}
 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 turns
 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
 interfaces.
 assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
 and     assm\<^isub>2: "P t"
 shows "Q t" (*<*)oops(*>*)
 text {*
-on the ML level:\footnote{Note that @{text "|>"} is reverse
+on the ML-level:\footnote{Note that @{text "|>"} is reverse
 application. This combinator, and several variants are defined in
 @{ML_file "Pure/General/basics.ML"}.}
 @{ML_response_fake [display]
 "let
 val thy = @{theory}
 val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
-val assm2 = cterm_of thy @{prop \"((P::nat\<Rightarrow>bool) t)\"}
+val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}
 val Pt_implies_Qt =
 assume assm1
 |> forall_elim (cterm_of thy @{term \"t::nat\"});
 A goal (or goal state) is a special @{ML_type thm}, which by
 convention is an implication of the form:
 @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
-where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals.
+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>
 prop"} is just the identity function and used as a syntactic marker.
-(FIXME: maybe show how this is printed on the screen)
 \begin{readmore}
 For more on goals see \isccite{sec:tactical-goals}.
 \end{readmore}
 Tactics are functions that map a goal state to a (lazy)
 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 from the tutorial~\cite{isa-tutorial} into ML:
 *}
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
 apply (erule disjE)
 apply (rule disjI2)

changeset 49	a0edabf14457
parent 48	609f9ef73494
child 50	3d4b49921cdb