isabelle-cookbook: comparison ProgTutorial/First

equal deleted inserted replaced

-:fb6c29a90003
+:d8c376662bb4
 theory First_Steps
 imports Base
 begin
-(*<*)
-setup{*
-open_file_with_prelude
-"First_Steps_Code.thy"
-["theory First_Steps", "imports Main", "begin"]
-*}
-(*>*)
 chapter {* First Steps\label{chp:firststeps} *}
 text {*
 \begin{flushright}
 we just use the functions @{ML_ind writeln in Pretty}  from the structure
 @{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
 @{ML_struct Syntax}. For more convenience, we bind them to the toplevel.
 *}
-ML{*val pretty_term = Syntax.pretty_term
+ML %grayML{*val pretty_term = Syntax.pretty_term
 val pwriteln = Pretty.writeln*}
 text {*
 They can now be used as follows
 If there is more than one term to be printed, you can use the
 function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty}
 to separate them.
 *}
-ML{*fun pretty_terms ctxt trms =
+ML %grayML{*fun pretty_terms ctxt trms =
 Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
 text {*
 You can also print out terms together with their typing information.
 For this you need to set the configuration value
 @{ML_ind show_types in Syntax} to @{ML true}.
 *}
-ML{*val show_types_ctxt = Config.put show_types true @{context}*}
+ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*}
 text {*
 Now by using this context @{ML pretty_term} prints out
 @{ML_response_fake [display, gray]
 \end{itemize}
 A @{ML_type cterm} can be printed with the following function.
 *}
-ML{*fun pretty_cterm ctxt ctrm =
+ML %grayML %grayML{*fun pretty_cterm ctxt ctrm =
 pretty_term ctxt (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}.
 *}
-ML{*fun pretty_cterms ctxt ctrms =
+ML %grayML{*fun pretty_cterms ctxt ctrms =
 Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))*}
 text {*
 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{*fun pretty_thm ctxt thm =
+ML %grayML{*fun pretty_thm ctxt thm =
 pretty_term ctxt (prop_of thm)*}
 text {*
 Theorems include schematic variables, such as @{text "?P"},
 @{text "?Q"} and so on. They are needed in Isabelle in order to able to
 However, in order to improve the readability when printing theorems, we
 can switch off the question marks as follows:
 *}
-ML{*fun pretty_thm_no_vars ctxt thm =
+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)
 end*}
 Again the functions @{ML commas} and @{ML block in Pretty} help
 with printing more than one theorem.
 *}
-ML{*fun pretty_thms ctxt thms =
+ML %grayML{*fun pretty_thms ctxt thms =
 Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
 fun pretty_thms_no_vars ctxt thms =
 Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*}
 text {*
 Printing functions for @{ML_type typ} are
 *}
-ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
+ML %grayML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
 fun pretty_typs ctxt tys =
 Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*}
 text {*
 respectively @{ML_type ctyp}
 *}
-ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
+ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
 fun pretty_ctyps ctxt ctys =
 Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
 text {*
 \begin{readmore}
 The simplest combinator is @{ML_ind I in Library}, which is just the
 identity function defined as
 *}
-ML{*fun I x = x*}
+ML %grayML{*fun I x = x*}
 text {*
 Another simple combinator is @{ML_ind K in Library}, defined as
 *}
-ML{*fun K x = fn _ => x*}
+ML %grayML{*fun K x = fn _ => x*}
 text {*
 @{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a
 result, @{ML K} defines a constant function always returning @{text x}.
 The next combinator is reverse application, @{ML_ind  "|>" in Basics}, defined as:
 *}
-ML{*fun x |> f = f x*}
+ML %grayML{*fun x |> f = f x*}
 text {* While just syntactic sugar for the usual function application,
 the purpose of this combinator is to implement functions in a
 ``waterfall fashion''. Consider for example the function *}
 manner. This kind of coding should be familiar, if you have been exposed to
 Haskell's {\it do}-notation. Writing the function @{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*}
+ML %grayML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 text {* or *}
-ML{*fun inc_by_five x =
+ML %grayML{*fun inc_by_five x =
 ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
 text {* and typographically more economical than *}
-ML{*fun inc_by_five x =
+ML %grayML{*fun inc_by_five x =
 let val y1 = x + 1
 val y2 = (y1, y1)
 val y3 = fst y2
 val y4 = y3 + 4
 in y4 end*}
 The combinator @{ML_ind "#>" in Basics} is the reverse function composition.
 It can be used to define the following function
 *}
-ML{*val inc_by_six =
+ML %grayML{*val inc_by_six =
 (fn x => x + 1) #>
 (fn x => x + 2) #>
 (fn x => x + 3)*}
 text {*
 The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},
 but applies a function to the value and returns the result together with the
 value (as a pair). It is defined as
 *}
-ML{*fun `f = fn x => (f x, x)*}
+ML %grayML{*fun `f = fn x => (f x, x)*}
 text {*
 An example for this combinator is the function
 *}
-ML{*fun inc_as_pair x =
+ML %grayML{*fun inc_as_pair x =
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))*}
 text {*
 which takes @{text x} as argument, and then increments @{text x}, but also keeps
 The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
 defined for functions manipulating pairs. The first applies the function to
 the first component of the pair, defined as
 *}
-ML{*fun (x, y) |>> f = (f x, y)*}
+ML %grayML{*fun (x, y) |>> f = (f x, y)*}
 text {*
 and the second combinator to the second component, defined as
 *}
-ML{*fun (x, y) ||> f = (x, f y)*}
+ML %grayML{*fun (x, y) ||> f = (x, f y)*}
 text {*
 These two functions can, for example, be used to avoid explicit @{text "lets"} for
 intermediate values in functions that return pairs. As an example, suppose you
 want to separate a list of integers into two lists according to a
 threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
 should be separated as @{ML "([1,2,3,4], [6,5])"}.  Such a function can be
 implemented as
 *}
-ML{*fun separate i [] = ([], [])
+ML %grayML{*fun separate i [] = ([], [])
 | separate i (x::xs) =
 let
 val (los, grs) = separate i xs
 in
 if i <= x then (los, x::grs) else (x::los, grs)
 where the return value of the recursive call is bound explicitly to
 the pair @{ML "(los, grs)" for los grs}. However, this function
 can be implemented more concisely as
 *}
-ML{*fun separate i [] = ([], [])
+ML %grayML{*fun separate i [] = ([], [])
 | separate i (x::xs) =
 if i <= x
 then separate i xs ||> cons x
 else separate i xs |>> cons x*}
 With the combinator @{ML_ind "|->" in Basics} you can re-combine the
 elements from a pair. This combinator is defined as
 *}
-ML{*fun (x, y) |-> f = f x y*}
+ML %grayML{*fun (x, y) |-> f = f x y*}
 text {*
 and can be used to write the following roundabout version
 of the @{text double} function:
 *}
-ML{*fun double x =
+ML %grayML{*fun double x =
 x |>  (fn x => (x, x))
 |-> (fn x => fn y => x + y)*}
 text {*
 The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your
 obtained by previous calls.
 A more realistic example for this combinator is the following code
 *}
-ML{*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.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
 Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
 function @{text double} can also be written as:
 *}
-ML{*val double =
+ML %grayML{*val double =
 (fn x => (x, x)) #->
 (fn x => fn y => x + y)*}
 text {*
 Note, however, that antiquotations are statically linked, that is their value is
 determined at ``compile-time'', not at ``run-time''. For example the function
 *}
-ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
+ML %grayML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 text {*
 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] "First_Steps"}, no matter where the
 It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
 whose first argument is a statement (possibly many of them separated by @{text "and"})
 and the second is a proof. For example
 *}
-ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
+ML %grayML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
 text {*
 The result can be printed out as follows.
 @{ML_response_fake [gray,display]
 You can also refer to the current simpset via an antiquotation. To illustrate
 this we implement the function that extracts the theorem names stored in a
 simpset.
 *}
-ML{*fun get_thm_names_from_ss simpset =
+ML %grayML{*fun get_thm_names_from_ss simpset =
 let
 val {simps,...} = Raw_Simplifier.dest_ss simpset
 in
 map #1 simps
 end*}
 which shows the internal representation of the term @{text "Suc ?x"}. Similarly
 we can write an antiquotation for type patterns. Its code is
 *}
-ML{*val type_pat_setup =
+ML %grayML{*val type_pat_setup =
 let
 val parser = Args.context -- Scan.lift Args.name_source
 fun typ_pat (ctxt, str) =
 let
 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}.
 *}
-ML{*local
+ML %grayML{*local
 val fn_int  = Universal.tag () : int  Universal.tag
 val fn_bool = Universal.tag () : bool Universal.tag
 in
 val inject_int   = Universal.tagInject fn_int;
 val inject_bool  = Universal.tagInject fn_bool;
 Using the injection functions, we can inject the integer @{ML_text "13"}
 and the boolean value @{ML_text "true"} into @{ML_type Universal.universal}, and
 then store them in a @{ML_type "Universal.universal list"} as follows:
 *}
-ML{*val foo_list =
+ML %grayML{*val foo_list =
 let
 val thirteen = inject_int 13
 val truth_val = inject_bool true
 in
 [thirteen, truth_val]
 it (@{ML Data.map}). There is also the functions @{ML Data.put}, which however is
 not relevant here. Below we define two
 auxiliary functions, which help us with accessing the table.
 *}
-ML{*val lookup = Symtab.lookup o Data.get
+ML %grayML{*val lookup = Symtab.lookup o Data.get
 fun update k v = Data.map (Symtab.update (k, v))*}
 text {*
 Since we want to store introduction rules associated with their
 logical connective, we can fill the table as follows.
 defeat its undo-mechanism. To see the latter, consider the
 following data container where we maintain a reference to a list of
 integers.
 *}
-ML{*structure WrongRefData = Theory_Data
+ML %grayML{*structure WrongRefData = Theory_Data
 (type T = (int list) Unsynchronized.ref
 val empty = Unsynchronized.ref []
 val extend = I
 val merge = fst)*}
 "ref []"}
 For updating the reference we use the following function
 *}
-ML{*fun ref_update n = WrongRefData.map
+ML %grayML{*fun ref_update n = WrongRefData.map
 (fn r => let val _ = r := n::(!r) in r end)*}
 text {*
 which takes an integer and adds it to the content of the reference.
 As before, we update the reference with the command
 Storing data in a proof context is done in a similar fashion. As mentioned
 before, the corresponding functor is @{ML_funct_ind Proof_Data}. With the
 following code we can store a list of terms in a proof context.
 *}
-ML{*structure Data = Proof_Data
+ML %grayML{*structure Data = Proof_Data
 (type T = term list
 fun init _ = [])*}
 text {*
 The init-function we have to specify must produce a list for when a context
 context is derived). We choose here to just return the empty list. Next
 we define two auxiliary functions for updating the list with a given
 term and printing the list.
 *}
-ML{*fun update trm = Data.map (fn trms => trm::trms)
+ML %grayML{*fun update trm = Data.map (fn trms => trm::trms)
 fun print ctxt =
 case (Data.get ctxt) of
 [] => pwriteln (Pretty.str "Empty!")
 | trms => pwriteln (pretty_terms ctxt trms)*}
 above. The first instance implements named theorem lists using the functor
 @{ML_funct_ind Named_Thms}. This is because storing theorems in a list
 is such a common task.  To obtain a named theorem list, you just declare
 *}
-ML{*structure FooRules = Named_Thms
+ML %grayML{*structure FooRules = Named_Thms
 (val name = @{binding "foo"}
 val description = "Theorems for foo") *}
 text {*
 and set up the @{ML_struct FooRules} with the command
 user to control three values, say @{text bval} containing a boolean, @{text
 ival} containing an integer and @{text sval} containing a string. These
 values can be declared by
 *}
-ML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
+ML %grayML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
 val ival = Attrib.setup_config_int @{binding "ival"} (K 0)
 val sval = Attrib.setup_config_string @{binding "sval"} (K "some string") *}
 text {*
 where each value needs to be given a default.

changeset 517	d8c376662bb4
parent 504	1d1165432c9f
child 538	e9fd5eff62c1