
diff -r 3ddf6c832c61 -r df09e49b19bf CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Sep 17 19:20:06 2008 -0400
+++ b/CookBook/FirstSteps.thy	Wed Sep 17 19:20:37 2008 -0400
@@ -26,8 +26,7 @@
 
 
 text {* 
-  Isabelle programming is done in Standard ML, however ML-code for Isabelle often
-  includes antiquotations to refer to the logical context of Isabelle. 
+  Isabelle programming is done in Standard ML.
   Just like lemmas and proofs, code in Isabelle is part of a 
   theory. If you want to follow the code written in this chapter, we 
   assume you are working inside the theory defined by
@@ -53,16 +52,39 @@
   The expression inside \isacommand{ML} commands is immediately evaluated,
   like ``normal'' Isabelle proof scripts, 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, on which the undo operation 
-  does not have any effect. 
+  can also contain value- and function bindings. However on such ML-commands the 
+  undo operation behaves slightly counter-intuitive, because if you define
+*}
+
+ML {*
+  val foo = true
 *}
 
+text {*
+  then Isabelle's undo operation has no effect on the definition of 
+  @{ML "foo"}. 
+
+  During coding you might find it necessary to quickly inspect some data
+  in your code. This can be done in a ``quick-and-dirty'' fashion using 
+  @{ML "warning"}. For example
+*}
+
+ML {*
+  val _ = warning "any string"
+*}
+
+text {*
+  will print out the string inside the response buffer of Isabelle.
+*}
+
+
+
 section {* Antiquotations *}
 
 text {*
-  The main advantage of embedding all code in a theory is that the
-  code can contain references to entities that are defined on the
-  logical level of Isabelle. This is done using antiquotations.
+  The main advantage of embedding all code 
+  in a theory is that the code can contain references to entities defined 
+  on the logical level of Isabelle. This is done using antiquotations.
   For example, one can print out the name of 
   the current theory by typing
 *}
@@ -75,7 +97,7 @@
   The name of this theory can be extrated using a the function @{ML "Context.theory_name"}. 
   So the code above returns the string @{ML "\"CookBook\""}.
 
-  Note that antiquotations are statically scoped, that is the value is
+  Note, however, that antiquotations are statically scoped, that is the value is
   determined at ``compile-time'' not ``run-time''. For example the function
 
 *}
@@ -93,6 +115,13 @@
   some data structure and return it. Instead, it is literally
   replaced with the value representing the theory name.
 
+  In a similar way you can use antiquotations to refer to types and theorems:
+*}
+
+ML {* @{typ "(int * nat) list"} *}
+ML {* @{thm allI} *}
+
+text {*
   In the course of this introduction, we will learn more about 
   these antoquotations: they greatly simplify Isabelle programming since one
   can directly access all kinds of logical elements from ML.
@@ -101,46 +130,37 @@
 section {* Terms *}
 
 text {*
-  We can simply quote Isabelle terms from ML using the @{text "@{term \<dots>}"} 
+  Terms of Isabelle can be constructed on the ML-level using the @{text "@{term \<dots>}"} 
   antiquotation:
 *}
 
 ML {* @{term "(a::nat) + b = c"} *}
 
 text {*
-  This shows the term @{term "(a::nat) + b = c"} in the internal
-  representation with all gory details. Terms are just an ML
-  datatype, and they are defined in @{ML_file "Pure/term.ML"}.
+  This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
+  representation of this term. This internal represenation is just a 
+  datatype defined in @{ML_file "Pure/term.ML"}.
   
-  The representation of terms uses deBruin indices: bound variables
-  are represented by the constructor @{ML Bound}, and the index refers to
-  the number of lambdas we have to skip until we hit the lambda that
-  binds the variable. The names of bound variables are kept at the
-  abstractions, but they should be treated just as comments. 
+  The internal representation of terms uses the usual deBruin indices mechanism: bound 
+  variables are represented by the constructor @{ML Bound} whose argument refers to
+  the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
+  binds the corresponding variable. However, the names of bound variables are 
+  kept at abstractions for printing purposes, and so should be treated just as comments. 
   See \ichcite{ch:logic} for more details.
 
+  (FIXME: Alex why is the reference bolow given. It somehow does not read
+  with what is written above.)
+
   \begin{readmore}
   Terms are described in detail in \ichcite{ch:logic}. Their
   definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
   \end{readmore}
 
-  In a similar way we can quote types and theorems:
-*}
-
-ML {* @{typ "(int * nat) list"} *}
-ML {* @{thm allI} *}
-
-text {* 
-  In the default setup, types and theorems are printed as strings. 
-*}
-
-
-text {*
   Sometimes the internal representation can be surprisingly different
   from what you see at the user level, because the layer of
-  parsing/type checking/pretty printing can be quite thick. 
+  parsing/type checking/pretty printing can be quite elaborate. 
 
-\begin{exercise}
+  \begin{exercise}
   Look at the internal term representation of the following terms, and
   find out why they are represented like this.
 
@@ -153,38 +173,46 @@
   Hint: The third term is already quite big, and the pretty printer
   may omit parts of it by default. If you want to see all of it, you
   can use @{ML "print_depth 50"} to set the limit to a value high enough.
-\end{exercise}
+  \end{exercise}
+
+  \begin{exercise}
+  Write a function @{ML_text "rev_sum : term -> term"} that takes a
+  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"}
+  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}.
+  Note that @{text "+"} associates to the left.
+  Try your function on some examples, and see if the result typechecks.
+  \end{exercise}
 *}
 
-section {* Type checking *}
+text {* FIXME: check possible solution *}
 
-text {* 
-  We can freely construct and manipulate terms, since they are just
-  arbitrary unchecked trees. However, we eventually want to see if a
-  term is wellformed in a certain context.
+ML {* 
+  exception FORM_ERROR 
 
-  Type checking is done via @{ML cterm_of}, which turns a @{ML_type
-  term} into a  @{ML_type cterm}, a \emph{certified} term. Unlike
-  @{ML_type term}s, which are just trees, @{ML_type
-  "cterm"}s are abstract objects that are guaranteed to be
-  type-correct, and can only be constructed via the official
-  interfaces.
-
-  Type
-  checking is always relative to a theory context. For now we can use
-  the @{ML "@{theory}"} antiquotation to get hold of the theory at the current
-  point:
+  fun rev_sum term =
+    case term of
+       @{term "op +"} $ (Free (x,t1)) $ (Free (y,t2)) => 
+                   @{term "op +"} $ (Free (y,t2)) $ (Free (x,t1))
+    |  @{term "op +"} $ left $ (Free (x,t)) => 
+                   @{term "op +"} $ (Free (x,t)) $ (rev_sum left)
+    |  _ => raise FORM_ERROR
 *}
 
-ML {*
-  let
-    val natT = @{typ "nat"}
-    val zero = @{term "0::nat"}(*Const ("HOL.zero_class.zero", natT)*)
-  in
-    cterm_of @{theory} 
-        (Const ("HOL.plus_class.plus", natT --> natT --> natT) 
-         $ zero $ zero)
-  end
+
+text {*
+  \begin{exercise}
+  Write a function which takes two terms representing natural numbers
+  in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
+  number representing their sum.
+  \end{exercise}
+
+  \begin{exercise}
+  Look at the functions defined in @{ML_file "Pure/logic.ML"} and
+  @{ML_file "HOL/hologic.ML"} and see if they can make your life
+  easier.
+  \end{exercise}
+
+  (FIXME what is coming next should fit with the main flow)
 *}
 
 ML {*
@@ -204,27 +232,37 @@
   another antiquotation: @{ML "@{const_name plus}"} gives just this
   name.
 
-  \begin{exercise}
-  Write a function @{ML_text "rev_sum : term -> term"} that takes a
-  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"}
-  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}.
-  Note that @{text "+"} associates to the left.
-  Try your function on some examples, and see if the result typechecks.
-  \end{exercise}
+  FIXME: maybe explain @{text "@{prop \<dots>}"} as a special kind of terms 
+*}
+
+ML {* @{prop "True"} *}
+
+
+
+
+section {* Type checking *}
+
+text {* 
+  We can freely construct and manipulate terms, since they are just
+  arbitrary unchecked trees. However, we eventually want to see if a
+  term is wellformed, or type checks, relative to a theory.
 
-  \begin{exercise}
-  Write a function which takes two terms representing natural numbers
-  in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
-  number representing their sum.
-  \end{exercise}
+  Type checking is done via the function @{ML cterm_of}, which turns 
+  a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
+  Unlike @{ML_type term}s, which are just trees, @{ML_type
+  "cterm"}s are abstract objects that are guaranteed to be
+  type-correct, and can only be constructed via the official
+  interfaces.
 
-  \begin{exercise}
-  Look at the functions defined in @{ML_file "Pure/logic.ML"} and
-  @{ML_file "HOL/hologic.ML"} and see if they can make your life
-  easier.
-  \end{exercise}
+  (FIXME: Alex what do you mean concretely by ``official interfaces'')
+
+  Type checking is always relative to a theory context. For now we can use
+  the @{ML "@{theory}"} antiquotation to get hold of the current theory.
+  For example we can write:
 *}
 
+ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}
+
 section {* Theorems *}
 
 text {*
@@ -236,10 +274,22 @@
 
   Using these rules, which are just ML functions, you can do simple
   natural deduction proofs on the ML level. For example, the statement
-  @{prop "(\<And>(x::nat). P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"} can be proved like
+*}
+
+  lemma 
+   assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
+   and     assm\<^isub>2: "P t"
+   shows "Q t"
+   (*<*)oops(*>*) 
+
+text {*
+  can be proved in ML like 
   this\footnote{Note that @{text "|>"} is just reverse
   application. This combinator, and several variants are defined in
   @{ML_file "Pure/General/basics.ML"}}:
+
+
+  (FIXME: Alex why did you not use antiquotations for this?)
 *}
 
 ML {*
@@ -271,6 +321,33 @@
 end
 *}
 
+ML {*
+
+let
+  val thy = @{theory}
+
+  val assm1 = cterm_of thy @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
+  val assm2 = cterm_of thy @{prop "((P::nat\<Rightarrow>bool) t)"}
+
+  val Pt_implies_Qt = 
+        assume assm1
+        |> forall_elim (cterm_of thy @{term "t::nat"});
+  
+  val Qt = implies_elim Pt_implies_Qt (assume assm2);
+in
+
+  Qt 
+  |> implies_intr assm2
+  |> implies_intr assm1
+end
+
+*}
+
+text {*
+  FIXME Explain this program more carefully
+*}
+
+
 section {* Tactical reasoning *}
 
 text {*




