isabelle-cookbook: comparison ProgTutorial/First

equal deleted inserted replaced

-:aec7073d4645
+:daf404920ab9
 imports Base
 begin
 chapter {* First Steps\label{chp:firststeps} *}
 text {*
 \begin{flushright}
 {\em ``The most effective debugging tool is still careful thought,\\
 coupled with judiciously placed print statements.''} \\[1ex]
 Brian Kernighan, in {\em Unix for Beginners}, 1979
 \end{flushright}
 \medskip
-Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
+Isabelle programming is done in ML @{cite "isa-imp"}. Just like lemmas and proofs, ML-code for
 Isabelle must be 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{quote}
 \begin{tabular}{@ {}l}
 A @{ML_type cterm} can be printed with the following function.
 *}
 ML %grayML %grayML{*fun pretty_cterm ctxt ctrm =
-pretty_term ctxt (term_of ctrm)*}
+pretty_term ctxt (Thm.term_of ctrm)*}
 text {*
 Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
 term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can be
 printed again with @{ML commas in Pretty}.
 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 in Thm}.
 *}
 ML %grayML{*fun pretty_thm ctxt thm =
-pretty_term ctxt (prop_of thm)*}
+pretty_term ctxt (Thm.prop_of thm)*}
 text {*
 Theorems include schematic variables, such as @{text "?P"},
 @{text "?Q"} and so on. They are instantiated by Isabelle when a theorem is applied.
 For example, the theorem
 ML %grayML{*fun pretty_thm_no_vars ctxt thm =
 let
 val ctxt' = Config.put show_question_marks false ctxt
 in
-pretty_term ctxt' (prop_of thm)
+pretty_term ctxt' (Thm.prop_of thm)
 end*}
 text {*
 With this function, theorem @{thm [source] conjI} is now printed as follows:
 text {*
 respectively @{ML_type ctyp}
 *}
-ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
+ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (Thm.typ_of cty)
 fun pretty_ctyps ctxt ctys =
 Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
 text {*
 \begin{readmore}
 obtained by previous calls.
 A more realistic example for this combinator is the following code
 *}
-ML %grayML{*val (((one_def, two_def), three_def), ctxt') =
+ML %grayML{*val ((([one_def], [two_def]), [three_def]), ctxt') =
 @{context}
-|> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
+|> Local_Defs.define [((@{binding "One"}, NoSyn), (Binding.empty_atts, @{term "1::nat"}))]
-||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
+||>> Local_Defs.define [((@{binding "Two"}, NoSyn), (Binding.empty_atts,@{term "2::nat"}))]
-||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
+||>> Local_Defs.define [((@{binding "Three"}, NoSyn), (Binding.empty_atts,@{term "3::nat"}))]*}
 text {*
 where we make three definitions, namely @{term "One \<equiv> 1::nat"}, @{term "Two \<equiv> 2::nat"}
 and @{term "Three \<equiv> 3::nat"}. The point of this code is that we augment the initial
 context with the definitions. The result we are interested in is the
 augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing
-information about the definitions---the function @{ML_ind add_def in Local_Defs} returns
+information about the definitions---the function @{ML_ind define in Local_Defs} returns
 both as pairs. We can use this information for example to print out the definiens and
 the theorem corresponding to the definitions. For example for the first definition:
 @{ML_response_fake [display, gray]
 "let
-val (one_trm, one_thm) = one_def
+val (one_trm, (_, one_thm)) = one_def
 in
 pwriteln (pretty_term ctxt' one_trm);
 pwriteln (pretty_thm ctxt' one_thm)
 end"
 "One
 \ref{chp:advanced}.) A context is for example needed to use the
 function @{ML print_abbrevs in Proof_Context} that list of all currently
 defined abbreviations. For example
 @{ML_response_fake [display, gray]
-"Proof_Context.print_abbrevs @{context}"
+"Proof_Context.print_abbrevs false @{context}"
 "\<dots>
 INTER \<equiv> INFI
 Inter \<equiv> Inf
 \<dots>"}
 for the antiquotation @{text "term_pat"} is as follows.
 *}
 ML %linenosgray{*val term_pat_setup =
 let
-val parser = Args.context -- Scan.lift Args.name_inner_syntax
+val parser = Args.context -- Scan.lift Args.embedded_inner_syntax
 fun term_pat (ctxt, str) =
 str |> Proof_Context.read_term_pattern ctxt
 |> ML_Syntax.print_term
 |> ML_Syntax.atomic
 we can write an antiquotation for type patterns. Its code is
 *}
 ML %grayML{*val type_pat_setup =
 let
-val parser = Args.context -- Scan.lift Args.name_inner_syntax
+val parser = Args.context -- Scan.lift Args.embedded_inner_syntax
 fun typ_pat (ctxt, str) =
 let
 val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
 in
 text {*
 However, a word of warning is in order: new antiquotations should be introduced only after
 careful deliberations. They can potentially make your code harder, rather than easier, to read.
-\begin{readmore}
+\begin{readmore} @{url "Norbert/ML/ml_antiquotation.ML"}
 The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
 contain the infrastructure and definitions for most antiquotations. Most of the basic operations
 on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
 \end{readmore}
 *}
 above it is important to keep in mind that the universal type does not
 destroy type-safety of ML: storing and accessing the data can only be done
 in a type-safe manner...though run-time checks are needed for that.
 \begin{readmore}
-In Isabelle the universal type is implemented as the type @{ML_type
+In ML the universal type is implemented as the type @{ML_type
-Universal.universal} in the file
+Universal.universal}.
-@{ML_file "Pure/ML-Systems/universal.ML"}.
 \end{readmore}
 We will show the usage of the universal type by storing an integer and
 a boolean into a single list. Let us first define injection and projection
 functions for booleans and integers into and from the type @{ML_type Universal.universal}.
 A concrete example for a configuration value is
 @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
 in the simplifier. This can be used for example in the following proof
 *}
 lemma
 shows "(False \<or> True) \<and> True"
 proof (rule conjI)
 show "False \<or> True" using [[simp_trace = true]] by simp
 next

changeset 562	daf404920ab9
parent 559	ffa5c4ec9611
child 564	6e2479089226