isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:2fff636e1fa0
+:ffd93dcc269d
 \ldots
 \end{tabular}
 \end{center}
 We also generally assume you are working with HOL. The given examples might
-need to be adapted slightly if you work in a different logic.
+need to be adapted if you work in a different logic.
 *}
 section {* Including ML-Code *}
 text {*
 \end{isabelle}
 Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
 evaluated by using the advance and undo buttons of 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
+value and function bindings, for example
-script is retracted. As mentioned in the Introduction, we will drop the
+*}
+ML %gray {*
+val r = ref 0
+fun f n = n + 1
+*}
+text {*
+and even those can be undone when the proof
+script is retracted.  As mentioned in the Introduction, we will drop the
 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
 show code. The lines prefixed with @{text [quotes] ">"} are not part of the
 code, rather they indicate what the response is when the code is evaluated.
 Once a portion of code is relatively stable, you usually want to export it
 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling})
 *}
 (*
+ML {* set Toplevel.debug *}
 ML {*
 fun dodgy_fun () = (raise (ERROR "bar"); 1)
 *}
-ML {* set Toplevel.debug *}
 ML {* fun f1 () = dodgy_fun () *}
 ML {* f1 () *}
 *)
 In the context of Isabelle, a ``real world'' example for a function written in
 the waterfall fashion might be the following code:
 *}
-ML %linenosgray{*fun apply_fresh_args pred ctxt =
+ML %linenosgray{*fun apply_fresh_args f ctxt =
-pred |> fastype_of
+f |> fastype_of
 |> binder_types
 |> map (pair "z")
-|> Variable.variant_frees ctxt [pred]
+|> Variable.variant_frees ctxt [f]
 |> map Free
-|> (curry list_comb) pred *}
+|> (curry list_comb) f *}
 text {*
-This code extracts the argument types of a given
+This code extracts the argument types of a given function and then generates
-predicate and then generates for each argument type a distinct variable; finally it
+for each argument type a distinct variable; finally it applies the generated
-applies the generated variables to the predicate. For example
+variables to the function. For example
 @{ML_response_fake [display,gray]
 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context}
 |> Syntax.string_of_term @{context}
 |> warning"
 "P z za zb"}
 You can read off this behaviour from how @{ML apply_fresh_args} is
 coded: in Line 2, the function @{ML fastype_of} calculates the type of the
-predicate; @{ML binder_types} in the next line produces the list of argument
+function; @{ML binder_types} in the next line produces the list of argument
 types (in the case above the list @{text "[nat, int, unit]"}); Line 4
 pairs up each type with the string  @{text "z"}; the
 function @{ML variant_frees in Variable} generates for each @{text "z"} a
-unique name avoiding the given @{text pred}; the list of name-type pairs is turned
+unique name avoiding the given @{text f}; the list of name-type pairs is turned
 into a list of variable terms in Line 6, which in the last line is applied
-by the function @{ML list_comb} to the predicate. We have to use the
+by the function @{ML list_comb} to the function. We have to use the
-function @{ML curry}, because @{ML list_comb} expects the predicate and the
+function @{ML curry}, because @{ML list_comb} expects the function and the
 variables list as a pair.
 The combinator @{ML "#>"} is the reverse function composition. It can be
 used to define the following function
 *}
 map #1 simps
 end*}
 text {*
 The function @{ML dest_ss in MetaSimplifier} returns a record containing all
-information stored in the simpset. We are only interested in the names of the
+information stored in the simpset, but we are only interested in the names of the
 simp-rules. So now you can feed in the current simpset into this function.
-The simpset can be referred to using the antiquotation @{text "@{simpset}"}.
+The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
 @{ML_response_fake [display,gray]
 "get_thm_names_from_ss @{simpset}"
 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 of lemmas to the simpset by the user that potentially cause loops.
 On the ML-level of Isabelle, you often have to work with qualified names;
 these are strings with some additional information, such positional information
 and qualifiers. Such bindings can be generated with the antiquotation
-@{text "@{bindin \<dots>}"}.
+@{text "@{binding \<dots>}"}.
 @{ML_response [display,gray]
 "@{binding \"name\"}"
 "name"}
 local_setup %gray {*
 snd o LocalTheory.define Thm.internalK
 ((@{binding "TrueConj"}, NoSyn),
 (Attrib.empty_binding, @{term "True \<and> True"})) *}
 text {*
+Now querying the definition you obtain:
+\begin{isabelle}
+\isacommand{thm}~@{text "TrueConj_def"}\\
+@{text "> "}@{thm TrueConj_def}
+\end{isabelle}
+(FIXME give a better example why bindings are important)
 While antiquotations have many applications, they were originally introduced in order
 to avoid explicit bindings for theorems such as:
 *}
 ML{*val allI = thm "allI" *}
 \begin{readmore}
 Terms are described in detail in \isccite{sec:terms}. Their
 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
 \end{readmore}
+Constructing terms via antiquotations has the advantage that only typable
+terms can be constructed. For example
+@{ML_response_fake_both [display,gray]
+"@{term \"(x::nat) x\"}"
+"Type unification failed \<dots>"}
+raises a typing error, while it perfectly ok to construct
+@{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"}
+with the raw ML-constructors.
 Sometimes the internal representation of terms can be surprisingly different
 from what you see at the user-level, because the layers of
 parsing/type-checking/pretty printing can be quite elaborate.
 \begin{exercise}
 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 where it is not (since it is already constructed by a meta-implication).
-Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:
+As already seen above, types can be constructed using the antiquotation
+@{text "@{typ \<dots>}"}. For example:
 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 \begin{readmore}
 Types are described in detail in \isccite{sec:types}. Their
 ML{*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} we obtain the intended term involving
+to both functions. With @{ML make_imp} you obtain the intended term involving
 the given arguments
 @{ML_response [display,gray] "make_imp @{term S} @{term T}"
 "Const \<dots> $
 Abs (\"x\", Type (\"nat\",[]),
 Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
-whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
+whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"}
 and @{text "Q"} from the antiquotation.
 @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}"
 "Const \<dots> $
 Abs (\"x\", \<dots>,
 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 There are a number of handy functions that are frequently used for
-constructing terms. One is the function @{ML list_comb} which a term
+constructing terms. One is the function @{ML list_comb}, which takes
-and a list of terms as argument, and produces as output the term
+a term and a list of terms as argument, and produces as output the term
 list applied to the term. For example
 @{ML_response_fake [display,gray]
 "list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
-(FIXME: handy functions for constructing terms:  @{ML lambda},
+Another handy function is @{ML lambda}, which abstracts a variable
-@{ML subst_free})
+in a term. For example
-*}
+@{ML_response_fake [display,gray]
-ML {* lambda @{term "x::nat"} @{term "P x"}*}
+"lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}"
+"Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
-text {*
+In the example @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}),
-As can be seen this function does not take the typing annotation into account.
+and an abstraction. It also records the type of the abstracted
+variable and for printing purposes also its name.  Note that because of the
+typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
+is of the same type as the abstracted variable. If it is of different type,
+as in
+@{ML_response_fake [display,gray]
+"lambda @{term \"x::nat\"} @{term \"(P::bool\<Rightarrow>bool) x\"}"
+"Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Free (\"x\", \"bool\"))"}
+then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted.
+This is a fundamental principle
+of Church-style typing, where variables with the same name still differ, if they
+have different type.
+There is also the function @{ML subst_free} with which terms can
+be replaced by other terms. For example below we replace in  @{term "f 0 x"}
+the subterm @{term "f 0"} by @{term y} and @{term x} by @{term True}.
+@{ML_response_fake [display,gray]
+"subst_free [(@{term \"(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0\"}, @{term \"y::nat\<Rightarrow>nat\"}),
+(@{term \"x::nat\"}, @{term \"True\"})]
+@{term \"((f::nat\<Rightarrow>nat\<Rightarrow>nat) 0) x\"}"
+"Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
+As can be seen, @{ML subst_free} does not take typability into account.
+However it takes alpha-equivalence into account:
+@{ML_response_fake [display, gray]
+"subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})]
+@{term \"(\<lambda>x::nat. x)\"}"
+"Free (\"x\", \"nat\")"}
 \begin{readmore}
 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
 and types easier.\end{readmore}
 Have a look at these files and try to solve the following two exercises:
-*}
-text {*
 \begin{exercise}\label{fun:revsum}
 Write a function @{text "rev_sum : term -> term"} that takes a
 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
 cterm_of @{theory}
 (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
 end" "0 + 0"}
 In Isabelle not just terms need to be certified, but also types. For example,
-you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on
+you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
 the ML-level as follows:
 @{ML_response_fake [display,gray]
 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
 "nat \<Rightarrow> bool"}
 \begin{exercise}
 Check that the function defined in Exercise~\ref{fun:revsum} returns a
 result that type-checks.
 \end{exercise}
-Remember Isabelle foolows the Church-style typing for terms, i.e.~a term contains
+Remember Isabelle follows the Church-style typing for terms, i.e.~a term contains
 enough typing information (constants, free variables and abstractions all have typing
 information) so that it is always clear what the type of a term is.
 Given a well-typed term, the function @{ML type_of} returns the
 type of a term. Consider for example:
 @{ML_response [display,gray]
 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 To calculate the type, this function traverses the whole term and will
-detect any typing inconsistency. For examle changing the type of the variable
+detect any typing inconsistency. For example changing the type of the variable
 @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message:
 @{ML_response_fake [display,gray]
 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
 end"
 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
 Instead of giving explicitly the type for the constant @{text "plus"} and the free
-variable @{text "x"}, the type-inference filles in the missing information.
+variable @{text "x"}, the type-inference fills in the missing information.
 \begin{readmore}
 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
-checking and pretty-printing of terms are defined. Fuctions related to the
+checking and pretty-printing of terms are defined. Functions related to the
 type inference are implemented in @{ML_file "Pure/type.ML"} and
 @{ML_file "Pure/type_infer.ML"}.
 \end{readmore}
 (FIXME: say something about sorts)
 *}
 section {* Theorem Attributes *}
 text {*
-Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text
+Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
-"[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
+"[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
 annotated to theorems, but functions that do further processing once a
-theorem is proven. In particular, it is not possible to find out
+theorem is proved. In particular, it is not possible to find out
 what are all theorems that have a given attribute in common, unless of course
-the function behind the attribute stores the theorems in a retrivable
+the function behind the attribute stores the theorems in a retrievable
 datastructure.
-If you want to print out all currently known attributes a theorem
+If you want to print out all currently known attributes a theorem can have,
-can have, you can use the function:
+you can use the Isabelle command
-@{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}"
+\begin{isabelle}
-"COMP:  direct composition with rules (no lifting)
+\isacommand{print\_attributes}\\
-HOL.dest:  declaration of Classical destruction rule
+@{text "> COMP:  direct composition with rules (no lifting)"}\\
-HOL.elim:  declaration of Classical elimination rule
+@{text "> HOL.dest:  declaration of Classical destruction rule"}\\
-\<dots>"}
+@{text "> HOL.elim:  declaration of Classical elimination rule"}\\
+@{text "> \<dots>"}
+\end{isabelle}
+The theorem attributes fall roughly into two categories: the first category manipulates
+the proved theorem (like @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
+stores the proved theorem somewhere as data (like @{text "[simp]"}, which adds
+the theorem to the current simpset).
 To explain how to write your own attribute, let us start with an extremely simple
 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
 returns another theorem (namely @{text thm} resolved with the lemma
 @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns
 an attribute.
 Before we can use the attribute, we need to set it up. This can be done
-using the function @{ML Attrib.setup} as follows.
+using the Isabelle command \isacommand{attribute\_setup} as follows:
 *}
-setup %gray {* Attrib.setup @{binding "my_sym"}
+attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *}
-(Scan.succeed my_symmetric) "applying the sym rule"*}
+"applying the sym rule"
 text {*
-The attribute does not expect any further arguments (unlike @{text "[OF
+The attribute does not expect any further arguments (unlike @{text "[THEN
-\<dots>]"}, for example, which can take a list of theorems as argument). Therefore
+\<dots>]"}, for example). Therefore
 we use the parser @{ML Scan.succeed}. Later on we will also consider
 attributes taking further arguments. An example for the attribute @{text
 "[my_sym]"} is the proof
 *}
 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
 text {*
-which stores the theorem @{thm test} under the name @{thm [source] test}. We
+which stores the theorem @{thm test} under the name @{thm [source] test}. You
-can also use the attribute when referring to this theorem.
+can see this, if you query the lemma:
+\begin{isabelle}
+\isacommand{thm}~@{text "test"}\\
+@{text "> "}~@{thm test}
+\end{isabelle}
+We can also use the attribute when referring to this theorem:
 \begin{isabelle}
 \isacommand{thm}~@{text "test[my_sym]"}\\
 @{text "> "}~@{thm test[my_sym]}
 \end{isabelle}
+As an example of a slightly more complicated theorem attribute, we implement
+our version of @{text "[THEN \<dots>]"}. This attribute takes a list of theorems
+as argument and resolves the proved theorem with this list (one theorem
+after another). The code for this attribute is:
+*}
+ML{*fun MY_THEN thms =
+Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
+text {*
+where @{ML swap} swaps the components of a pair. The setup of this theorem
+attribute uses the parser @{ML Attrib.thms}, which parses a list of
+theorems.
+*}
+attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
+"resolving the list of theorems with the proved theorem"
+text {*
+You can, for example, use this theorem attribute to turn an equation into a
+meta-equation:
+\begin{isabelle}
+\isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\
+@{text "> "}~@{thm test[MY_THEN eq_reflection]}
+\end{isabelle}
+If you need the symmetric version as a meta-equation, you can write
+\begin{isabelle}
+\isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\
+@{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
+\end{isabelle}
+Of course, it is also possible to combine different theorem attributes, as in:
+\begin{isabelle}
+\isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
+@{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
+\end{isabelle}
+However, here also a weakness of the concept
+of theorem attributes show through: since theorem attributes can be an
+arbitrary functions, they do not in general commute. If you try
+\begin{isabelle}
+\isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
+@{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
+\end{isabelle}
+you get an exception indicating that the theorem @{thm [source] sym}
+does not resolve with meta-equations.
 The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
 Another usage of attributes is to add and delete theorems from stored data.
 For example the attribute @{text "[simp]"} adds or deletes a theorem from the
 current simpset. For these applications, you can use @{ML Thm.declaration_attribute}.
 To illustrate this function, let us introduce a reference containing a list
 of theorems.
 *}
-ML{*val my_thms = ref ([]:thm list)*}
+ML{*val my_thms = ref ([] : thm list)*}
 text {*
 A word of warning: such references must not be used in any code that
 is meant to be more than just for testing purposes! Here it is only used
 to illustrate matters. We will show later how to store data properly without
-using references. The function @{ML Thm.declaration_attribute} expects us to
+using references.
+The function @{ML Thm.declaration_attribute} expects us to
 provide two functions that add and delete theorems from this list.
 For this we use the two functions:
 *}
 ML{*fun my_thms_add thm ctxt =
 text {*
 and set up the attributes as follows
 *}
-setup %gray {* Attrib.setup @{binding "my_thms"}
+attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
-(Attrib.add_del my_add my_del) "maintaining a list of my_thms" *}
+"maintaining a list of my_thms"
 text {*
 Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
 *}
 However, as said at the beginning of this example, using references for storing theorems is
 \emph{not} the received way of doing such things. The received way is to
 start a ``data slot'' in a context by using the functor @{text GenericDataFun}:
 *}
-ML {*structure Data = GenericDataFun
+ML {*structure MyThmsData = GenericDataFun
 (type T = thm list
 val empty = []
 val extend = I
 fun merge _ = Thm.merge_thms) *}
 text {*
 To use this data slot, you only have to change @{ML my_thms_add} and
 @{ML my_thms_del} to:
 *}
-ML{*val thm_add = Data.map o Thm.add_thm
+ML{*val thm_add = MyThmsData.map o Thm.add_thm
-val thm_del = Data.map o Thm.del_thm*}
+val thm_del = MyThmsData.map o Thm.del_thm*}
 text {*
-where @{ML Data.map} updates the data appropriately in the context. Since storing
+where @{ML MyThmsData.map} updates the data appropriately in the context. The
+theorem addtributes are
+*}
+ML{*val add = Thm.declaration_attribute thm_add
+val del = Thm.declaration_attribute thm_del *}
+text {*
+ad the setup is as follows
+*}
+attribute_setup %gray my_thms2 = {* Attrib.add_del add del *}
+"properly maintaining a list of my_thms"
+ML {* MyThmsData.get (Context.Proof @{context}) *}
+lemma [my_thms2]: "2 = Suc (Suc 0)" by simp
+ML {* MyThmsData.get (Context.Proof @{context}) *}
+ML {* !my_thms *}
+text {*
+(FIXME: explain problem with backtracking)
+Since storing
 theorems in a special list is such a common task, there is the functor @{text NamedThmsFun},
 which does most of the work for you. To obtain such a named theorem lists, you just
 declare
 *}

changeset 193	ffd93dcc269d
parent 192	2fff636e1fa0
child 194	8cd51a25a7ca