isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:fb6c29a90003
+:d8c376662bb4
 theory Essential
 imports Base First_Steps
 begin
-(*<*)
-setup{*
-open_file_with_prelude
-"Essential_Code.thy"
-["theory Essential", "imports Base First_Steps", "begin"]
-*}
-(*>*)
 chapter {* Isabelle Essentials *}
 text {*
 \begin{flushright}
 function below we mimic the behaviour of the usual pretty printer for
 datatypes (it uses pretty-printing functions which will be explained in more
 detail in Section~\ref{sec:pretty}).
 *}
-ML{*local
+ML %grayML{*local
 fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
 fun pp_list xs = Pretty.list "[" "]" xs
 fun pp_str s   = Pretty.str s
 fun pp_qstr s  = Pretty.quote (pp_str s)
 fun pp_int i   = pp_str (string_of_int i)
 text {*
 We can install this pretty printer with the function
 @{ML_ind addPrettyPrinter in PolyML} as follows.
 *}
-ML{*PolyML.addPrettyPrinter
+ML %grayML{*PolyML.addPrettyPrinter
 (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}
 text {*
 Now the type bool is printed out in full detail.
 We can restore the usual behaviour of Isabelle's pretty printer
 with the code
 *}
-ML{*PolyML.addPrettyPrinter
+ML %grayML{*PolyML.addPrettyPrinter
 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}
 text {*
 After that the types for booleans, lists and so on are printed out again
 the standard Isabelle way.
 function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
 @{term P} and @{term Q} as arguments can only be written as:
 *}
-ML{*fun make_imp P Q =
+ML %grayML{*fun make_imp P Q =
 let
 val x = Free ("x", @{typ nat})
 in
 Logic.all x (Logic.mk_implies (P $ x, Q $ x))
 end *}
 The reason is that you cannot pass the arguments @{term P} and @{term Q}
 into an antiquotation.\footnote{At least not at the moment.} For example
 the following does \emph{not} work.
 *}
-ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
+ML %grayML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
 text {*
 To see this, apply @{text "@{term S}"} and @{text "@{term T}"}
 to both functions. With @{ML make_imp} you obtain the intended term involving
 the given arguments
 Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound
 variables with terms. To see how this function works, let us implement a
 function that strips off the outermost forall quantifiers in a term.
 *}
-ML{*fun strip_alls t =
+ML %grayML{*fun strip_alls t =
 let
 fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
 in
 case t of
 Const (@{const_name All}, _) $ Abs body => aux body
 Note that we produced in the body two dangling de Bruijn indices.
 Later on we will also use the inverse function that
 builds the quantification from a body and a list of (free) variables.
 *}
-ML{*fun build_alls ([], t) = t
+ML %grayML{*fun build_alls ([], t) = t
 | build_alls (Free (x, T) :: vs, t) =
 Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool})
 $ Abs (x, T, build_alls (vs, t))*}
 text {*
 constants. They usually crop up when pattern matching terms or types, or
 when constructing them. While it is perfectly ok to write the function
 @{text is_true} as follows
 *}
-ML{*fun is_true @{term True} = true
+ML %grayML{*fun is_true @{term True} = true
 | is_true _ = false*}
 text {*
 this does not work for picking out @{text "\<forall>"}-quantified terms. Because
 the function
 *}
-ML{*fun is_all (@{term All} $ _) = true
+ML %grayML{*fun is_all (@{term All} $ _) = true
 | is_all _ = false*}
 text {*
 will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}:
 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for
 an arbitrary, but fixed type @{typ "'a"}. A properly working alternative
 for this function is
 *}
-ML{*fun is_all (Const ("HOL.All", _) $ _) = true
+ML %grayML{*fun is_all (Const ("HOL.All", _) $ _) = true
 | is_all _ = false*}
 text {*
 because now
 However there is still a problem: consider the similar function that
 attempts to pick out @{text "Nil"}-terms:
 *}
-ML{*fun is_nil (Const ("Nil", _)) = true
+ML %grayML{*fun is_nil (Const ("Nil", _)) = true
 | is_nil _ = false *}
 text {*
 Unfortunately, also this function does \emph{not} work as expected, since
 variable parts of the constant's name. Therefore a function for
 matching against constants that have a polymorphic type should
 be written as follows.
 *}
-ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
+ML %grayML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
 | is_nil_or_all _ = false *}
 text {*
 The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
 when defining constants. For example the function returning a function
 type is as follows:
 *}
-ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
+ML %grayML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
 text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}
-ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
+ML %grayML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
 text {*
 If you want to construct a function type with more than one argument
 type, then you can use @{ML_ind "--->" in Term}.
 *}
-ML{*fun make_fun_types tys ty = tys ---> ty *}
+ML %grayML{*fun make_fun_types tys ty = tys ---> ty *}
 text {*
 A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a
 function and applies it to every type in a term. You can, for example,
 change every @{typ nat} in a term into an @{typ int} using the function:
 *}
-ML{*fun nat_to_int ty =
+ML %grayML{*fun nat_to_int ty =
 (case ty of
 @{typ nat} => @{typ int}
 | Type (s, tys) => Type (s, map nat_to_int tys)
 | _ => ty)*}
 text_raw {*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}*}
-ML{*fun pretty_helper aux env =
+ML %grayML{*fun pretty_helper aux env =
 env |> Vartab.dest
 |> map aux
 |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])
 |> Pretty.enum "," "[" "]"
 |> pwriteln
 *}
 class s1
 class s2
-ML{*val (tyenv, index) = let
+ML %grayML{*val (tyenv, index) = let
 val ty1 = @{typ_pat "?'a::s1"}
 val ty2 = @{typ_pat "?'b::s2"}
 in
 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
 end*}
 also from the structure @{ML_struct Sign}. This function returns a @{ML_type
 Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case
 of failure. For example
 *}
-ML{*val tyenv_match = let
+ML %grayML{*val tyenv_match = let
 val pat = @{typ_pat "?'a * ?'b"}
 and ty  = @{typ_pat "bool list * nat"}
 in
 Sign.typ_match @{theory} (pat, ty) Vartab.empty
 end*}
 @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir}
 for unifiers. To show the difference, let us calculate the
 following matcher:
 *}
-ML{*val tyenv_match' = let
+ML %grayML{*val tyenv_match' = let
 val pat = @{typ_pat "?'a * ?'b"}
 and ty  = @{typ_pat "?'b list * nat"}
 in
 Sign.typ_match @{theory} (pat, ty) Vartab.empty
 end*}
 first_order_match in Pattern} for terms.  This matching function returns a
 type environment and a term environment.  To pretty print the latter we use
 the function @{text "pretty_env"}:
 *}
-ML{*fun pretty_env ctxt env =
+ML %grayML{*fun pretty_env ctxt env =
 let
 fun get_trms (v, (T, t)) = (Var (v, T), t)
 val print = pairself (pretty_term ctxt)
 in
 pretty_helper (print o get_trms) env
 a schematic term variable with a type and a term.  An example of a first-order
 matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern
 @{text "?X ?Y"}.
 *}
-ML{*val (_, fo_env) = let
+ML %grayML{*val (_, fo_env) = let
 val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
 val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"}
 val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
 val init = (Vartab.empty, Vartab.empty)
 in
 not posses a single most general solution. Therefore Isabelle implements the
 unification function @{ML_ind unifiers in Unify} so that it returns a lazy
 list of potentially infinite unifiers.  An example is as follows
 *}
-ML{*val uni_seq =
+ML %grayML{*val uni_seq =
 let
 val trm1 = @{term_pat "?X ?Y"}
 val trm2 = @{term "f a"}
 val init = Envir.empty 0
 in
 The unifiers can be extracted from the lazy sequence using the
 function @{ML_ind "Seq.pull"}. In the example we obtain three
 unifiers @{text "un1\<dots>un3"}.
 *}
-ML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
+ML %grayML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
 val SOME ((un2, _), next2) = Seq.pull next1;
 val SOME ((un3, _), next3) = Seq.pull next2;
 val NONE = Seq.pull next3 *}
 text {*
 from an environment the corresponding variable mappings for schematic type
 and term variables. These mappings can be turned into proper
 @{ML_type ctyp}-pairs with the function
 *}
-ML{*fun prep_trm thy (x, (T, t)) =
+ML %grayML{*fun prep_trm thy (x, (T, t)) =
 (cterm_of thy (Var (x, T)), cterm_of thy t)*}
 text {*
 and into proper @{ML_type cterm}-pairs with
 *}
-ML{*fun prep_ty thy (x, (S, ty)) =
+ML %grayML{*fun prep_ty thy (x, (S, ty)) =
 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}
 text {*
 We can now calculate the instantiations from the matching function.
 *}
 also implements a mechanism where a theorem name can refer to a custom theorem
 list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}.
 To see how it works let us assume we defined our own theorem list @{text MyThmList}.
 *}
-ML{*structure MyThmList = Generic_Data
+ML %grayML{*structure MyThmList = Generic_Data
 (type T = thm list
 val empty = []
 val extend = I
 val merge = merge Thm.eq_thm_prop)
 @{text "?list"}. For this we can use the function
 @{ML_ind forall_intr_vars in Drule}. This allows us to implement the
 following function for atomizing a theorem.
 *}
-ML{*fun atomize_thm thm =
+ML %grayML{*fun atomize_thm thm =
 let
 val thm' = forall_intr_vars thm
 val thm'' = Object_Logic.atomize (cprop_of thm')
 in
 Raw_Simplifier.rewrite_rule [thm''] thm'
 There is also the possibility of proving multiple goals at the same time
 using the function @{ML_ind prove_multi in Goal}. For this let us define the
 following three helper functions.
 *}
-ML{*fun rep_goals i = replicate i @{prop "f x = f x"}
+ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
 fun rep_tacs i = replicate i (rtac @{thm refl})
 fun multi_test ctxt i =
 Goal.prove_multi ctxt ["f", "x"] [] (rep_goals i)
 (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*}
 large goals. If you increase the counter in the code above to @{text 3000},
 you will notice that takes approximately ten(!) times longer than
 using @{ML map} and @{ML prove in Goal}.
 *}
-ML{*let
+ML %grayML{*let
 fun test_prove ctxt thm =
 Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1))
 in
 map (test_prove @{context}) (rep_goals 3000)
 end*}
 giving a list of strings that should be used for the replacement of the
 variables. For this we implement the function which takes a list of strings
 and uses them as name in the outermost abstractions.
 *}
-ML{*fun rename_allq [] t = t
+ML %grayML{*fun rename_allq [] t = t
 | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) =
 Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
 | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
 rename_allq xs t
 | rename_allq _ t = t*}
 version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
 to produce the ``symmetric'' version of an equation. The main function behind
 this attribute is
 *}
-ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
+ML %grayML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
 text {*
 where the function @{ML_ind  rule_attribute in Thm} expects a function taking a
 context (which we ignore in the code above) and a theorem (@{text thm}), and
 returns another theorem (namely @{text thm} resolved with the theorem
 An alternative for setting up an attribute is the function @{ML_ind  setup in Attrib}.
 So instead of using \isacommand{attribute\_setup}, you can also set up the
 attribute as follows:
 *}
-ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
+ML %grayML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
 "applying the sym rule" *}
 text {*
 This gives a function from @{ML_type "theory -> theory"}, which
 can be used for example with \isacommand{setup} or with
 our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
 as argument and resolve the theorem with this list (one theorem
 after another). The code for this attribute is
 *}
-ML{*fun MY_THEN thms =
+ML %grayML{*fun MY_THEN thms =
 let
 fun RS_rev thm1 thm2 = thm2 RS thm1
 in
 Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)
 end*}
 or deletes a theorem from the current simpset. For these applications, you
 can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,
 let us introduce a theorem list.
 *}
-ML{*structure MyThms = Named_Thms
+ML %grayML{*structure MyThms = Named_Thms
 (val name = @{binding "attr_thms"}
 val description = "Theorems for an Attribute") *}
 text {*
 We are going to modify this list by adding and deleting theorems.
 For this we use the two functions @{ML MyThms.add_thm} and
 @{ML MyThms.del_thm}. You can turn them into attributes
 with the code
 *}
-ML{*val my_add = Thm.declaration_attribute MyThms.add_thm
+ML %grayML{*val my_add = Thm.declaration_attribute MyThms.add_thm
 val my_del = Thm.declaration_attribute MyThms.del_thm *}
 text {*
 and set up the attributes as follows
 *}
 string}. This can be done with the function @{ML_ind  string_of in Pretty}. In what
 follows we will use the following wrapper function for printing a pretty
 type:
 *}
-ML{*fun pprint prt = tracing (Pretty.string_of prt)*}
+ML %grayML{*fun pprint prt = tracing (Pretty.string_of prt)*}
 text {*
 The point of the pretty-printing infrastructure is to give hints about how to
 layout text and let Isabelle do the actual layout. Let us first explain
 how you can insert places where a line break can occur. For this assume the
 following function that replicates a string n times:
 *}
-ML{*fun rep n str = implode (replicate n str) *}
+ML %grayML{*fun rep n str = implode (replicate n str) *}
 text {*
 and suppose we want to print out the string:
 *}
-ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
+ML %grayML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
 text {*
 We deliberately chose a large string so that it spans over more than one line.
 If we print out the string using the usual ``quick-and-dirty'' method, then
 we obtain the ugly output:

changeset 517	d8c376662bb4
parent 513	f223f8223d4a
child 529	13d7ea419c5f