
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)"
   "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> 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 \<dots>}"}-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: "\<forall>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
-(\<lambda>x. x) = (\<lambda>x. x)"}
+  "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
 
   Other function produce terms that can be pattern-matched. 
   Suppose the following two theorems.
@@ -899,16 +900,14 @@
   and   foo_test2: "A \<longrightarrow> B \<longrightarrow> 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 "\<verbopen> \<dots> \<verbclose>"}.} 
-*}  
-
-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 "\<verbopen> \<dots> \<verbclose>"}.} 
+*}  
+
+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) *}
 




