# HG changeset patch # User Christian Urban # Date 1255516418 -7200 # Node ID 2f2018927f2a13d2e35c5023c0bb85b13f4d3f5d # Parent 01e71cddf6a3ea0b2c3ceec3dedbd3527f00ecc4 tuned diff -r 01e71cddf6a3 -r 2f2018927f2a ProgTutorial/General.thy --- a/ProgTutorial/General.thy Wed Oct 14 02:32:53 2009 +0200 +++ b/ProgTutorial/General.thy Wed Oct 14 12:33:38 2009 +0200 @@ -779,8 +779,7 @@ final statement of the theorem. @{ML_response_fake [display, gray] - "string_of_thm @{context} my_thm -|> tracing" + "tracing (string_of_thm @{context} my_thm)" "\\x. P x \ Q x; P t\ \ Q t"} However, internally the code-snippet constructs the following @@ -801,7 +800,7 @@ While we obtained a theorem as result, this theorem is not yet stored in Isabelle's theorem database. Consequently, it cannot be - referenced later on. One way to store it in the theorem database is + referenced on the user level. One way to store it in the theorem database is by using the function @{ML_ind note in LocalTheory}. *} @@ -811,14 +810,15 @@ 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 - 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: + classifies the theorem. There are several such kind indicators: for a + theorem arising from a definition we should 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 of @{ML note in LocalTheory} is the name under which we store the + theorem or theorems. The third argument can contain a list of (theorem) + attributes. We will explain them in detail in + Section~\ref{sec:attributes}. Below we just use one such attribute in order add + the theorem to the simpset: *} local_setup %gray {* @@ -827,11 +827,13 @@ [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 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. + Note that we have to use another name under which the theorem is stored, + since Isabelle does not allow us 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 @@ -853,14 +855,14 @@ 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. + this theorem on the user-level. We will see later on that usually we have to + construct meta-variables in theorems 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. + we can test theorems for alpha equality. Suppose you proved the following three + theorems. *} lemma @@ -869,7 +871,7 @@ and thm3: "\y. Q y" sorry text {* - Testing for equality using the function @{ML_ind eq_thm in Thm} produces: + Testing them for alpha equality using the function @{ML_ind eq_thm in Thm} produces: @{ML_response [display,gray] "(Thm.eq_thm (@{thm thm1}, @{thm thm2}), @@ -885,10 +887,9 @@ val eq = @{thm True_def} in (Thm.lhs_of eq, Thm.rhs_of eq) - |> pairself (tracing o string_of_cterm @{context}) + |> pairself (string_of_cterm @{context}) end" - "True -(\x. x) = (\x. x)"} + "(True, (\x. x) = (\x. x))"} Other function produce terms that can be pattern-matched. Suppose the following two theorems. @@ -899,16 +900,14 @@ and foo_test2: "A \ B \ C" sorry text {* - We can deconstruct them into premises and conclusions as follows. + We can destruct them into premises and conclusions as follows. @{ML_response_fake [display,gray] "let val ctxt = @{context} fun prems_and_concl thm = - [\"Premises: \" ^ - (string_of_terms ctxt (Thm.prems_of thm))] @ - [\"Conclusion: \" ^ - (string_of_term ctxt (Thm.concl_of thm))] + [\"Premises: \" ^ (string_of_terms ctxt (Thm.prems_of thm))] @ + [\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))] |> cat_lines |> tracing in @@ -1080,59 +1079,6 @@ oops -section {* Setups (TBD) *} - -text {* - In the previous section we used \isacommand{setup} in order to make - a theorem attribute known to Isabelle. What happens behind the scenes - is that \isacommand{setup} expects a function of type - @{ML_type "theory -> theory"}: the input theory is the current theory and the - output the theory where the theory attribute has been stored. - - This is a fundamental principle in Isabelle. A similar situation occurs - for example with declaring constants. The function that declares a - constant on the ML-level is @{ML_ind add_consts_i in Sign}. - If you write\footnote{Recall that ML-code needs to be - enclosed in \isacommand{ML}~@{text "\ \ \"}.} -*} - -ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *} - -text {* - for declaring the constant @{text "BAR"} with type @{typ nat} and - run the code, then you indeed obtain a theory as result. But if you - query the constant on the Isabelle level using the command \isacommand{term} - - \begin{isabelle} - \isacommand{term}~@{text [quotes] "BAR"}\\ - @{text "> \"BAR\" :: \"'a\""} - \end{isabelle} - - you do not obtain a constant of type @{typ nat}, but a free variable (printed in - blue) of polymorphic type. The problem is that the ML-expression above did - not register the declaration with the current theory. This is what the command - \isacommand{setup} is for. The constant is properly declared with -*} - -setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *} - -text {* - Now - - \begin{isabelle} - \isacommand{term}~@{text [quotes] "BAR"}\\ - @{text "> \"BAR\" :: \"nat\""} - \end{isabelle} - - returns a (black) constant with the type @{typ nat}. - - A similar command is \isacommand{local\_setup}, which expects a function - of type @{ML_type "local_theory -> local_theory"}. Later on we will also - use the commands \isacommand{method\_setup} for installing methods in the - current theory and \isacommand{simproc\_setup} for adding new simprocs to - the current simpset. -*} - section {* Theorem Attributes\label{sec:attributes} *} text {* @@ -1358,7 +1304,58 @@ \end{readmore} *} +section {* Setups (TBD) *} +text {* + In the previous section we used \isacommand{setup} in order to make + a theorem attribute known to Isabelle. What happens behind the scenes + is that \isacommand{setup} expects a function of type + @{ML_type "theory -> theory"}: the input theory is the current theory and the + output the theory where the theory attribute has been stored. + + This is a fundamental principle in Isabelle. A similar situation occurs + for example with declaring constants. The function that declares a + constant on the ML-level is @{ML_ind add_consts_i in Sign}. + If you write\footnote{Recall that ML-code needs to be + enclosed in \isacommand{ML}~@{text "\ \ \"}.} +*} + +ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *} + +text {* + for declaring the constant @{text "BAR"} with type @{typ nat} and + run the code, then you indeed obtain a theory as result. But if you + query the constant on the Isabelle level using the command \isacommand{term} + + \begin{isabelle} + \isacommand{term}~@{text [quotes] "BAR"}\\ + @{text "> \"BAR\" :: \"'a\""} + \end{isabelle} + + you do not obtain a constant of type @{typ nat}, but a free variable (printed in + blue) of polymorphic type. The problem is that the ML-expression above did + not register the declaration with the current theory. This is what the command + \isacommand{setup} is for. The constant is properly declared with +*} + +setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *} + +text {* + Now + + \begin{isabelle} + \isacommand{term}~@{text [quotes] "BAR"}\\ + @{text "> \"BAR\" :: \"nat\""} + \end{isabelle} + + returns a (black) constant with the type @{typ nat}. + + A similar command is \isacommand{local\_setup}, which expects a function + of type @{ML_type "local_theory -> local_theory"}. Later on we will also + use the commands \isacommand{method\_setup} for installing methods in the + current theory and \isacommand{simproc\_setup} for adding new simprocs to + the current simpset. +*} section {* Theories (TBD) *} diff -r 01e71cddf6a3 -r 2f2018927f2a ProgTutorial/ROOT.ML --- a/ProgTutorial/ROOT.ML Wed Oct 14 02:32:53 2009 +0200 +++ b/ProgTutorial/ROOT.ML Wed Oct 14 12:33:38 2009 +0200 @@ -28,5 +28,5 @@ use_thy "Recipes/USTypes"; use_thy "Solutions"; -use_thy "Readme"; +(*use_thy "Readme";*) diff -r 01e71cddf6a3 -r 2f2018927f2a progtutorial.pdf Binary file progtutorial.pdf has changed