
diff -r ebbd0dd008c8 -r fee4942c4770 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Thu Jan 29 09:46:17 2009 +0000
+++ b/CookBook/FirstSteps.thy	Thu Jan 29 09:46:36 2009 +0000
@@ -7,7 +7,7 @@
 text {*
 
   Isabelle programming is done in ML.  Just like lemmas and proofs, ML-code
-  in Isabelle is part of a theory. If you want to follow the code written in
+  in Isabelle is part of a theory. If you want to follow the code given in
   this chapter, we assume you are working inside the theory starting with
 
   \begin{center}
@@ -26,7 +26,7 @@
 
 text {*
   The easiest and quickest way to include code in a theory is
-  by using the \isacommand{ML}-command. For example\smallskip
+  by using the \isacommand{ML}-command. For example:
 
 \begin{isabelle}
 \begin{graybox}
@@ -37,17 +37,17 @@
 \end{graybox}
 \end{isabelle}
 
-  Like ``normal'' Isabelle proof scripts, 
+  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 script is retracted. As mentioned earlier, we will  
   drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} 
-  whenever we show code.
+  scaffolding whenever we show code.
 
   Once a portion of code is relatively stable, one usually wants to 
   export it to a separate ML-file. Such files can then be included in a 
-  theory by using \isacommand{uses} in the header of the theory, like
+  theory by using the \isacommand{uses}-command in the header of the theory, like:
 
   \begin{center}
   \begin{tabular}{@ {}l}
@@ -85,7 +85,7 @@
   output this function generates will be overwritten as soon as an error is
   raised. For printing anything more serious and elaborate, the
   function @{ML tracing} is more appropriate. This function writes all output into
-  a separate tracing buffer. For example
+  a separate tracing buffer. For example:
 
   @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 
@@ -111,7 +111,7 @@
   Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
   will cause that all tracing information is printed into the file @{text "foo.bar"}.
 
-  Error messages can be printed using the function @{ML error}, as in
+  You can print out error messages with the function @{ML error}, as in:
 
   @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
 
@@ -134,10 +134,10 @@
  
   where @{text "@{theory}"} is an antiquotation that is substituted with the
   current theory (remember that we assumed we are inside the theory 
-  @{text FirstSteps}). The name of this theory can be extracted with
+  @{text FirstSteps}). The name of this theory can be extracted using
   the function @{ML "Context.theory_name"}. 
 
-  Note, however, that antiquotations are statically scoped, that is their value is
+  Note, however, that antiquotations are statically linked, that is their value is
   determined at ``compile-time'', not ``run-time''. For example the function
 *}
 
@@ -145,7 +145,7 @@
 
 text {*
 
-  does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a 
+  does \emph{not} return the name of the current theory, if it is run in a 
   different theory. Instead, the code above defines the constant function 
   that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
   function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
@@ -161,12 +161,12 @@
 
   @{ML_response_fake [display,gray] 
 "let
-  val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
+  val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset}
 in
   map #name (Net.entries rules)
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
-  The code about simpsets extracts the theorem names that are stored in the
+  The code about simpsets extracts the theorem names stored in the
   current simpset.  We get hold of the current simpset with the antiquotation 
   @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
   containing all information about the simpset. The rules of a simpset are
@@ -182,20 +182,20 @@
   \end{readmore}
 
   While antiquotations have many applications, they were originally introduced in order 
-  to avoid explicit bindings for theorems such as
+  to avoid explicit bindings for theorems such as:
 *}
 
 ML{*val allI = thm "allI" *}
 
 text {*
   These bindings are difficult to maintain and also can be accidentally
-  overwritten by the user. This often breakes definitional
+  overwritten by the user. This often breakes Isabelle
   packages. Antiquotations solve this problem, since they are ``linked''
-  statically at compile-time. However, this static linkage also limits their
-  usefulness in cases where data needs to be build up dynamically. In the course of 
-  this introduction, we will learn more about
-  these antiquotations: they greatly simplify Isabelle programming since one
-  can directly access all kinds of logical elements from ML.
+  statically at compile-time.  However, this static linkage also limits their
+  usefulness in cases where data needs to be build up dynamically. In the
+  course of this introduction, we will learn more about these antiquotations:
+  they greatly simplify Isabelle programming since one can directly access all
+  kinds of logical elements from th ML-level.
 
 *}
 
@@ -203,7 +203,7 @@
 
 text {*
   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
-  \mbox{@{text "@{term \<dots>}"}}. For example
+  \mbox{@{text "@{term \<dots>}"}}. For example:
 
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
@@ -231,7 +231,7 @@
 
   \begin{exercise}
   Look at the internal term representation of the following terms, and
-  find out why they are represented like this.
+  find out why they are represented like this:
 
   \begin{itemize}
   \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}  
@@ -261,7 +261,7 @@
 
   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
+  Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:
 
   @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
@@ -279,11 +279,11 @@
   While antiquotations are very convenient for constructing terms, they can
   only construct fixed terms (remember they are ``linked'' at
   compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external}
-  for a function that pattern-matches over terms and where the pattern are
-  constructed from antiquotations.  However, one often needs to construct
+  for a function that pattern-matches over terms and where the patterns are
+  constructed using antiquotations.  However, one often needs to construct
   terms dynamically. For example, a function that returns the implication
   @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term
-  "\<tau>"} as arguments can only be written as
+  "\<tau>"} as arguments can only be written as:
 *}
 
 ML{*fun make_imp P Q tau =
@@ -294,7 +294,6 @@
   end *}
 
 text {*
-
   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
   @{term "tau"} into an antiquotation. For example the following does \emph{not} work:
 *}
@@ -357,7 +356,7 @@
 text {*
 
   \begin{readmore}
-  There are many functions in @{ML_file "Pure/logic.ML"} and
+  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
   and types easier.\end{readmore}
 
@@ -381,8 +380,23 @@
   number representing their sum.
   \end{exercise}
 
+  (FIXME: maybe should go)
 
-  (FIXME: operation from page 19 of the implementation manual)
+*}
+
+ML{*fun nat_to_int t =
+  (case t of
+     @{typ nat} => @{typ int}
+   | Type (s, ts) => Type (s, map nat_to_int ts)
+   | _ => t)*}
+
+text {*
+
+@{ML_response_fake [display,gray] 
+"map_types nat_to_int @{term \"a = (1::nat)\"}" 
+"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
+           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
+
 *}
 
 section {* Type-Checking *}
@@ -431,7 +445,7 @@
   result that type-checks.
   \end{exercise}
 
-  (FIXME: @{text "ctyp_of"})
+  (FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
 
 *}
 
@@ -676,13 +690,33 @@
 ML{*val double =
             (fn x => (x, x))
         #-> (fn x => fn y => x + y)*}
-  
 
 text {*
   
-
-
   (FIXME: find a good exercise for combinators)
 *}
 
+
+(*<*)
+setup {*
+ Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] 
+*}
+
+lemma "bar = (1::nat)"
+  oops
+
+setup {*   
+  Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
+ #> PureThy.add_defs false [((Binding.name "foo_def", 
+       Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
+ #> snd
+*}
+
+lemma "foo = (1::nat)"
+  apply(simp add: foo_def)
+  done
+
+thm foo_def
+(*>*)
+
 end
\ No newline at end of file




