
diff -r 4ae1ecb71539 -r 163ac0662211 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Wed Oct 07 09:54:01 2009 +0200
+++ b/ProgTutorial/General.thy	Wed Oct 07 11:28:40 2009 +0200
@@ -9,7 +9,6 @@
   theorem proving where there is a small trusted core and everything else is
   build on top of this trusted core. The central data structures involved
   in this core are certified terms and types as well as theorems.
-
 *}
 
 
@@ -185,7 +184,7 @@
 text {*
   While antiquotations are very convenient for constructing terms, they can
   only construct fixed terms (remember they are ``linked'' at compile-time).
-  However, you often need to construct terms dynamically. For example, a
+  However, you often need to construct terms manually. For example, a
   function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
   @{term P} and @{term Q} as arguments can only be written as:
 
@@ -573,62 +572,6 @@
 section {* Type-Checking\label{sec:typechecking} *}
 
 text {* 
-  
-  You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
-  typ}es, since they are just arbitrary unchecked trees. However, you
-  eventually want to see if a term is well-formed, or type-checks, relative to
-  a theory.  Type-checking is done via the function @{ML_ind  cterm_of}, which
-  converts 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 they can only
-  be constructed via ``official interfaces''.
-
-
-  Type-checking is always relative to a theory context. For now we use
-  the @{ML "@{theory}"} antiquotation to get hold of the current theory.
-  For example you can write:
-
-  @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"}
-
-  This can also be written with an antiquotation:
-
-  @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
-
-  Attempting to obtain the certified term for
-
-  @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
-
-  yields an error (since the term is not typable). A slightly more elaborate
-  example that type-checks is:
-
-@{ML_response_fake [display,gray] 
-"let
-  val natT = @{typ \"nat\"}
-  val zero = @{term \"0::nat\"}
-in
-  cterm_of @{theory} 
-      (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
-end" "0 + 0"}
-
-  In Isabelle not just terms need to be certified, but also types. For example, 
-  you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
-  the ML-level as follows:
-
-  @{ML_response_fake [display,gray]
-  "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
-  "nat \<Rightarrow> bool"}
-
-  or with the antiquotation:
-
-  @{ML_response_fake [display,gray]
-  "@{ctyp \"nat \<Rightarrow> bool\"}"
-  "nat \<Rightarrow> bool"}
-
-  \begin{readmore}
-  For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
-  the file @{ML_file "Pure/thm.ML"}.
-  \end{readmore}
-
   Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 
   enough typing information (constants, free variables and abstractions all have typing 
   information) so that it is always clear what the type of a term is. 
@@ -689,6 +632,7 @@
   \end{readmore}
 
   \footnote{\bf FIXME: say something about sorts.}
+  \footnote{\bf FIXME: give a ``readmore''.}
 
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
@@ -698,6 +642,88 @@
   \end{exercise}
 *}
 
+section {* Certified Terms and Certified Types *}
+
+text {*
+  You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
+  typ}es, since they are just arbitrary unchecked trees. However, you
+  eventually want to see if a term is well-formed, or type-checks, relative to
+  a theory.  Type-checking is done via the function @{ML_ind  cterm_of}, which
+  converts 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 they can only
+  be constructed via ``official interfaces''.
+
+  Certification is always relative to a theory context. For example you can 
+  write:
+
+  @{ML_response_fake [display,gray] 
+  "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" 
+  "a + b = c"}
+
+  This can also be written with an antiquotation:
+
+  @{ML_response_fake [display,gray] 
+  "@{cterm \"(a::nat) + b = c\"}" 
+  "a + b = c"}
+
+  Attempting to obtain the certified term for
+
+  @{ML_response_fake_both [display,gray] 
+  "@{cterm \"1 + True\"}" 
+  "Type unification failed \<dots>"}
+
+  yields an error (since the term is not typable). A slightly more elaborate
+  example that type-checks is:
+
+@{ML_response_fake [display,gray] 
+"let
+  val natT = @{typ \"nat\"}
+  val zero = @{term \"0::nat\"}
+in
+  cterm_of @{theory} 
+      (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
+end" "0 + 0"}
+
+  In Isabelle not just terms need to be certified, but also types. For example, 
+  you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
+  the ML-level as follows:
+
+  @{ML_response_fake [display,gray]
+  "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
+  "nat \<Rightarrow> bool"}
+
+  or with the antiquotation:
+
+  @{ML_response_fake [display,gray]
+  "@{ctyp \"nat \<Rightarrow> bool\"}"
+  "nat \<Rightarrow> bool"}
+
+  Since certified terms are, unlike terms, abstract objects, we cannot
+  pattern-match against them. However, we can construct them. For example
+  the function @{ML_ind capply in Thm} produces a certified application.
+
+  @{ML_response_fake [display,gray]
+  "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
+  "P 3"}
+
+  Similarly @{ML_ind list_comb in Drule} applies a list of @{ML_type cterm}s.
+
+  @{ML_response_fake [display,gray]
+  "let
+  val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"}
+  val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}]
+in
+  Drule.list_comb (chead, cargs)
+end"
+  "P () 3"}
+
+  \begin{readmore}
+  For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
+  the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and
+  @{ML_file "Pure/drule.ML"}.
+  \end{readmore}
+*}
 
 section {* Theorems *}
 
@@ -1445,7 +1471,7 @@
 
 
 
-section {* Name Space Issues (TBD) *}
+section {* Managing Name Spaces (TBD) *}
 
 
 end




