
diff -r 05cbe2430b76 -r 1ca2f41770cc ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Aug 19 00:49:40 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 19 09:25:49 2009 +0200
@@ -864,20 +864,19 @@
   "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
 
   the indices refer to the number of Abstractions (@{ML Abs}) that we need to
-  skip until we hit the @{ML Abs} that binds the corresponding variable. Constructing 
-  a term with dangling de Bruijn indices is possible, but will be flagged as
-  ill-formed when you try to typecheck or certify it (see
-  Section~\ref{sec:typechecking}). Note that the names of bound variables are kept at
-  abstractions for printing purposes, and so should be treated only as
-  ``comments''.  Application in Isabelle is realised with the term-constructor
-  @{ML $}.
-
+  skip until we hit the @{ML Abs} that binds the corresponding
+  variable. Constructing a term with dangling de Bruijn indices is possible,
+  but will be flagged as ill-formed when you try to typecheck or certify it
+  (see Section~\ref{sec:typechecking}). Note that the names of bound variables
+  are kept at abstractions for printing purposes, and so should be treated
+  only as ``comments''.  Application in Isabelle is realised with the
+  term-constructor @{ML $}.
 
   Isabelle makes a distinction between \emph{free} variables (term-constructor
-  @{ML Free} and written in blue colour) and \emph{schematic} variables
-  (term-constructor @{ML Var} and written with a leading question mark). The
-  latter correspond to the schematic variables that when printed show up with
-  a question mark in front of them. Consider the following two examples
+  @{ML Free} and written on the user level in blue colour) and
+  \emph{schematic} variables (term-constructor @{ML Var} and written with a
+  leading question mark). Consider the following two examples
+
 
   
   @{ML_response_fake [display, gray]
@@ -891,10 +890,13 @@
 end"
 "?x3, ?x1.3, x"}
 
-  When constructing terms, you are usually concerned with free variables (as mentioned earlier,
-  you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). 
-  If you deal with theorems, you have to, however, observe the distinction. A similar
-  distinction holds for types (see below).
+  When constructing terms, you are usually concerned with free variables (as
+  mentioned earlier, you cannot construct schematic variables using the
+  antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,
+  however, observe the distinction. The reason is that only schematic
+  varaibles can be instantiated with terms when a theorem is applied. A
+  similar distinction between free and schematic variables holds for types
+  (see below).
 
   \begin{readmore}
   Terms and types are described in detail in \isccite{sec:terms}. Their
@@ -944,8 +946,8 @@
   @{ML [display,gray] "print_depth 50"}
   \end{exercise}
 
-  The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
-  inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
+  The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 
+  usually invisible @{text "Trueprop"}-coercions whenever necessary. 
   Consider for example the pairs
 
 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
@@ -955,9 +957,13 @@
   where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
-  "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
+  "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, 
+ Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 
   where it is not (since it is already constructed by a meta-implication). 
+  The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
+  an object logic, for example HOL, into the meta-logic of Isabelle. It
+  is needed whenever a term is constructed that will be proved as a theorem. 
 
   As already seen above, types can be constructed using the antiquotation 
   @{text "@{typ \<dots>}"}. For example:
@@ -1091,11 +1097,11 @@
 
   @{ML_response_fake [display,gray]
 "let
-  val s1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
-  val s2 = (@{term \"x::nat\"}, @{term \"True\"})
+  val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
+  val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
   val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
 in
-  subst_free [s1, s2] trm
+  subst_free [sub1, sub2] trm
 end"
   "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
 
@@ -1104,10 +1110,10 @@
 
   @{ML_response_fake [display, gray]
 "let
-  val s = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
+  val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
   val trm = @{term \"(\<lambda>x::nat. x)\"}
 in
-  subst_free [s] trm
+  subst_free [sub] trm
 end"
   "Free (\"x\", \"nat\")"}
 
@@ -1117,7 +1123,7 @@
 *}
 
 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
-     strip_alls t |>> cons (Free (n, T))
+         strip_alls t |>> cons (Free (n, T))
   | strip_alls t = ([], t) *}
 
 text {*
@@ -1156,7 +1162,8 @@
 "let
   val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
-  tracing (string_of_term @{context} eq)
+  string_of_term @{context} eq
+  |> tracing
 end"
   "True = False"}
 *}
@@ -1167,31 +1174,6 @@
   in @{ML_file "HOL/Tools/hologic.ML"}.
   \end{readmore}
 
-  \begin{exercise}\label{ex:debruijn}
-  Implement the function,\footnote{Personal communication of
-  de Bruijn to Dyckhoff.} called deBruijn n, that constructs terms of the form:
-  
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  {\it rhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n.  P\,i}\\
-  {\it lhs n} & $\dn$ & $\bigwedge${\it i=1\ldots n. P\,i = P (i + 1 mod n)}
-                        $\longrightarrow$ {\it rhs n}\\
-  {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\
-  \end{tabular}
-  \end{center}
-
-  For n=3 this function returns the term
-
-  \begin{center}
-  \begin{tabular}{l}
-  (P 2 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\
-  (P 1 = P 2 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\wedge$\\ 
-  (P 1 = P 3 $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1) $\longrightarrow$ P 3 $\wedge$ P 2 $\wedge$ P 1
-  \end{tabular}
-  \end{center}
-
-  \end{exercise}
-
   When constructing terms manually, there are a few subtle issues with
   constants. They usually crop up when pattern matching terms or types, or
   when constructing them. While it is perfectly ok to write the function
@@ -1279,23 +1261,8 @@
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
-  and types easier.\end{readmore}
-
-  Have a look at these files and try to solve the following two exercises:
-
-  \begin{exercise}\label{fun:revsum}
-  Write a function @{text "rev_sum : term -> term"} that takes a
-  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
-  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
-  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
-  associates to the left. Try your function on some examples. 
-  \end{exercise}
-
-  \begin{exercise}\label{fun:makesum}
-  Write a function which takes two terms representing natural numbers
-  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
-  number representing their sum.
-  \end{exercise}
+  and types easier.
+  \end{readmore}
 
   The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
   For example
@@ -1380,6 +1347,47 @@
   be easily folded over a list of terms. Similarly for all functions
   named @{text "add_*"} in @{ML_file "Pure/term.ML"}.
 
+  \begin{exercise}\label{fun:revsum}
+  Write a function @{text "rev_sum : term -> term"} that takes a
+  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
+  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
+  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
+  associates to the left. Try your function on some examples. 
+  \end{exercise}
+
+  \begin{exercise}\label{fun:makesum}
+  Write a function which takes two terms representing natural numbers
+  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
+  number representing their sum.
+  \end{exercise}
+
+  \begin{exercise}\footnote{Personal communication of
+  de Bruijn to Dyckhoff.}\label{ex:debruijn}
+  Implement the function, which we below name deBruijn, that depends on a natural
+  number n$>$0 and constructs terms of the form:
+  
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  {\it rhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n.  P\,i}\\
+  {\it lhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i = P (i + 1 mod n)}
+                        $\longrightarrow$ {\it rhs n}\\
+  {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\
+  \end{tabular}
+  \end{center}
+
+  For n=3 this function returns the term
+
+  \begin{center}
+  \begin{tabular}{l}
+  (P 1 = P 2 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\
+  (P 2 = P 3 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\ 
+  (P 3 = P 1 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3
+  \end{tabular}
+  \end{center}
+
+  Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}
+  for constructing the terms for the logical connectives. 
+  \end{exercise}
 *}
 
 




