# HG changeset patch # User Christian Urban # Date 1255480373 -7200 # Node ID 01e71cddf6a3ea0b2c3ceec3dedbd3527f00ecc4 # Parent 0fea8b7a14a1a8c2eb6a47bb43934d2a8220bc1e slightly tuned diff -r 0fea8b7a14a1 -r 01e71cddf6a3 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Tue Oct 13 22:57:25 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Wed Oct 14 02:32:53 2009 +0200 @@ -17,7 +17,7 @@ {\em ``We will most likely never realize the full importance of painting the Tower,\\ that it is the essential element in the conservation of metal works and the\\ - more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex] + more meticulous the paint job, the longer the tower shall endure.''} \\[1ex] Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been re-painted 18 times since its initial construction, an average of once every seven years. It takes more than a year for a team of 25 painters to paint the tower @@ -214,7 +214,7 @@ *) text {* - Most often you want to inspect data of Isabelle's most basic data + Most often you want to inspect data of Isabelle's basic data structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they @@ -1045,11 +1045,11 @@ text {* which takes an integer and adds it to the content of the reference. - As above we update the reference with the command + As done above, we update the reference with the command \isacommand{setup}. *} -setup %gray{* ref_update 1 *} +setup %gray {* ref_update 1 *} text {* A lookup in the current theory gives then the expected list @@ -1059,13 +1059,13 @@ "WrongRefData.get @{theory}" "ref [1]"} - So far everything is as expected. But, the trouble starts if we attempt - to backtrack to ``before'' the \isacommand{setup}-command. There, we - would expect that the list is empty again. But since it is stored in - a reference, Isabelle has no control over it. So it is not - empty, but still @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, - if we execute the \isacommand{setup}-command again, we do not obtain - @{ML "ref [1]" in Unsynchronized}, but + So far everything is as expected. But, the trouble starts if we attempt to + backtrack to the point ``before'' the \isacommand{setup}-command. There, we + would expect that the list is empty again. But since it is stored in a + reference, Isabelle has no control over it. So it is not empty, but still + @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the + \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in + Unsynchronized}, but @{ML_response_fake [display,gray] "WrongRefData.get @{theory}" @@ -1080,7 +1080,7 @@ The functors for data storage are defined in @{ML_file "Pure/context.ML"}. Isabelle contains implementations of several container data structures, including association lists in @{ML_file "Pure/General/alist.ML"}, - directed graphs in @{ML_file "Pure/General/graph.ML"}. and + directed graphs in @{ML_file "Pure/General/graph.ML"}, and tables and symtables in @{ML_file "Pure/General/table.ML"}. \end{readmore} @@ -1114,16 +1114,16 @@ @{ML_response_fake [display,gray] "let - val ctxt = @{context} - val ctxt' = ctxt |> update @{term \"False\"} - |> update @{term \"True \ True\"} - val ctxt'' = ctxt |> update @{term \"1::nat\"} - val ctxt''' = ctxt'' |> update @{term \"2::nat\"} + val ctxt0 = @{context} + val ctxt1 = ctxt0 |> update @{term \"False\"} + |> update @{term \"True \ True\"} + val ctxt2 = ctxt0 |> update @{term \"1::nat\"} + val ctxt3 = ctxt2 |> update @{term \"2::nat\"} in - print ctxt; - print ctxt'; - print ctxt''; - print ctxt''' + print ctxt0; + print ctxt1; + print ctxt2; + print ctxt3 end" "Empty! True \ True, False @@ -1138,8 +1138,7 @@ associated data. This is different to theories, where the command \isacommand{setup} registers the data with the current and future theories, and therefore one can access the data potentially - indefinitely.\footnote{\bf FIXME: check this; it seems that is in - conflict with the statements below.} + indefinitely. For convenience there is an abstract layer, the type @{ML_type Context.generic}, for theories and proof contexts. This type is defined as follows @@ -1199,18 +1198,24 @@ On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}: *} -setup %gray {* - Context.theory_map (FooRules.add_thm @{thm TrueI}) -*} +setup %gray {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *} text {* The rules in the list can be retrieved using the function @{ML FooRules.get}: - @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"True\", \"?C\",\"?B\"]"} + @{ML_response_fake [display,gray] + "FooRules.get @{context}" + "[\"True\", \"?C\",\"?B\"]"} + + Note that this function takes a proof context as argument. This might be + confusing, since the theorem list is stored as theory data. The proof context + however conatains the information about the current theory and so the function + can access the theorem list in the theory via the context. \begin{readmore} - For more information see @{ML_file "Pure/Tools/named_thms.ML"}. + For more information about named theorem lists see + @{ML_file "Pure/Tools/named_thms.ML"}. \end{readmore} The second special instance of the data storage mechanism are configuration @@ -1251,24 +1256,25 @@ "Config.get @{context} bval" "true"} - or from a theory using the function @{ML_ind get_thy in Config} + or directly from a theory using the function @{ML_ind get_thy in Config} @{ML_response [display,gray] "Config.get_thy @{theory} bval" "true"} It is also possible to manipulate the configuration values - from the ML-level with the function @{ML_ind put in Config} - or @{ML_ind put_thy in Config}. For example + from the ML-level with the functions @{ML_ind put in Config} + and @{ML_ind put_thy in Config}. For example @{ML_response [display,gray] "let val ctxt = @{context} val ctxt' = Config.put sval \"foo\" ctxt + val ctxt'' = Config.put sval \"bar\" ctxt' in - (Config.get ctxt sval, Config.get ctxt' sval) + (Config.get ctxt sval, Config.get ctxt' sval, Config.get ctxt'' sval) end" - "(\"some string\", \"foo\")"} + "(\"some string\", \"foo\", \"bar\")"} \begin{readmore} For more information about configuration values see @@ -1287,9 +1293,13 @@ contains mechanisms for storing arbitrary data in theory and proof contexts. - This chapter also mentions two coding conventions: namely printing - entities belonging together as one string, and not using references - in any Isabelle code. + \begin{conventions} + \begin{itemize} + \item Print messages that belong together as a single string. + \item Do not use references in any Isabelle code. + \end{itemize} + \end{conventions} + *} diff -r 0fea8b7a14a1 -r 01e71cddf6a3 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Tue Oct 13 22:57:25 2009 +0200 +++ b/ProgTutorial/General.thy Wed Oct 14 02:32:53 2009 +0200 @@ -11,7 +11,7 @@ (*>*) -chapter {* Isabelle in More Detail \mbox{or, the Good, the Bad and the Ugly} *} +chapter {* Isabelle in More Detail *} text {* Isabelle is build around a few central ideas. One central idea is the @@ -693,7 +693,7 @@ val zero = @{term \"0::nat\"} in cterm_of @{theory} - (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) + (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, @@ -779,7 +779,8 @@ final statement of the theorem. @{ML_response_fake [display, gray] - "string_of_thm @{context} my_thm |> tracing" + "string_of_thm @{context} my_thm +|> tracing" "\\x. P x \ Q x; P t\ \ Q t"} However, internally the code-snippet constructs the following @@ -811,24 +812,26 @@ text {* The first argument @{ML_ind theoremK in Thm} is a kind indicator, which classifies the theorem. For a theorem arising from a definition we should - state @{ML_ind definitionK in Thm}, instead. The second argument is the - name under which we store the theorem or theorems. The third can contain - a list of (theorem) attributes. Above it is empty, but if we want to store - the theorem and at the same time add it to the simpset we have to declare: + use @{ML_ind definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, for + ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK + in Thm}. The second argument is the name under which we store the theorem + or theorems. The third can contain a list of (theorem) attributes. We will + explain them in detail in Section~\ref{sec:attributes}. Below we + use such an attribute in order add the theorem to the simpset. + have to declare: *} local_setup %gray {* LocalTheory.note Thm.theoremK - ((@{binding "my_thm_simp"}, - [Attrib.internal (K Simplifier.simp_add)]), - [my_thm]) #> snd *} + ((@{binding "my_thm_simp"}, + [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *} text {* Note that we have to use another name for the theorem, since Isabelle does - not allow to add another theorem under the same name. The attribute can be - given @{ML_ind internal in Attrib}. If we use the function @{ML - get_thm_names_from_ss} from the previous chapter, we can check whether the - theorem has been added. + not allow to store another theorem under the same name. The attribute needs to + be wrapped inside the function @{ML_ind internal in Attrib}. If we use the + function @{ML get_thm_names_from_ss} from the previous chapter, we can check + whether the theorem has actually been added. @{ML_response [display,gray] "let @@ -838,20 +841,23 @@ end" "true"} - Now the theorems @{thm [source] my_thm} and @{thm [source] my_thm_simp} can - also be referenced with the \isacommand{thm}-command on the user-level of - Isabelle + The main point of storing the theorems @{thm [source] my_thm} and @{thm + [source] my_thm_simp} is that they can now also be referenced with the + \isacommand{thm}-command on the user-level of Isabelle + \begin{isabelle} \isacommand{thm}~@{text "my_thm"}\isanewline @{text ">"}~@{prop "\\x. P x \ Q x; P t\ \ Q t"} \end{isabelle} - or with the @{text "@{thm \}"}-antiquotation on the ML-level. Note that the - theorem does not have any meta-variables that would be present if we proved - this theorem on the user-level. As we shall see later on, we have to construct - meta-variables explicitly. + or with the @{text "@{thm \}"}-antiquotation on the ML-level. As can be seen + the theorem does not have any meta-variables that would be present if we proved + this theorem on the user-level. We will see later on, we have to construct + meta-variables in a theorem explicitly. +*} +text {* There is a multitude of functions that manage or manipulate theorems. For example we can test theorems for (alpha) equality. Suppose you proved the following three facts. @@ -922,6 +928,16 @@ @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. \end{readmore} + The simplifier can be used to unfold definition in theorms. To show + this we build the theorem @{term "True \ True"} (Line 1) and then + unfold the constant according to its definition (Line 2). + + @{ML_response_fake [display,gray,linenos] + "Thm.reflexive @{cterm \"True\"} + |> Simplifier.rewrite_rule [@{thm True_def}] + |> string_of_thm @{context} + |> tracing" + "(\x. x) = (\x. x) \ (\x. x) = (\x. x)"} Often it is necessary to transform theorems to and from the object logic. For example, the function @{ML_ind rulify in ObjectLogic} @@ -946,10 +962,32 @@ In this code the function @{ML atomize in ObjectLogic} produces a meta-equation between the given theorem and the theorem transformed - into the object logic. The function @{ML_ind rewrite_rule in MetaSimplifier} - unfolds this meta-equation in the given theorem. The result is - the theorem with object logic connectives. -x + into the object logic. The result is the theorem with object logic + connectives. However, in order to completely transform a theorem + such as @{thm [source] list.induct} + + @{thm [display] list.induct} + + we have to first abstract over the variables @{text "?P"} and + @{text "?list"}. For this we can use the function + @{ML_ind forall_intr_vars in Drule}. +*} + +ML{*fun atomize_thm thm = +let + val thm' = forall_intr_vars thm + val thm'' = ObjectLogic.atomize (cprop_of thm') +in + MetaSimplifier.rewrite_rule [thm''] thm' +end*} + +text {* + For @{thm [source] list.induct} it produces: + + @{ML_response_fake [display, gray] + "atomize_thm @{thm list.induct}" + "\P list. P [] \ (\a list. P list \ P (a # list)) \ P list"} + Theorems can also be produced from terms by giving an explicit proof. One way to achive this is by using the function @{ML_ind prove in Goal}. For example diff -r 0fea8b7a14a1 -r 01e71cddf6a3 ProgTutorial/document/root.tex --- a/ProgTutorial/document/root.tex Tue Oct 13 22:57:25 2009 +0200 +++ b/ProgTutorial/document/root.tex Wed Oct 14 02:32:53 2009 +0200 @@ -74,6 +74,8 @@ \newenvironment{readmore}% {\begin{leftrightbar}\small\it{\textbf{Read More}}\\}{\end{leftrightbar}} +\newenvironment{conventions}% +{\begin{leftrightbar}\small\it{\textbf{Coding Conventions}}}{\end{leftrightbar}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % some mathematical notation \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}} diff -r 0fea8b7a14a1 -r 01e71cddf6a3 progtutorial.pdf Binary file progtutorial.pdf has changed