
diff -r d69214e47ef9 -r efb5fff99c96 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Thu Aug 20 23:30:51 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Fri Aug 21 11:42:14 2009 +0200
@@ -831,1638 +831,4 @@
   own document antiquotations. 
 *}
 
-section {* Terms and Types *}
-
-text {*
-  One way to construct Isabelle terms, is by using the antiquotation 
-  \mbox{@{text "@{term \<dots>}"}}. For example
-
-  @{ML_response [display,gray] 
-"@{term \"(a::nat) + b = c\"}" 
-"Const (\"op =\", \<dots>) $ 
-  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
-
-  will show the term @{term "(a::nat) + b = c"}, but printed using the internal
-  representation corresponding to the datatype @{ML_type  "term"} defined as follows: 
-*}  
-
-ML_val %linenosgray{*datatype term =
-  Const of string * typ 
-| Free of string * typ 
-| Var of indexname * typ 
-| Bound of int 
-| Abs of string * typ * term 
-| $ of term * term *}
-
-text {*
-  This datatype implements lambda-terms typed in Church-style.
-  As can be seen in Line 5, terms use the usual de Bruijn index mechanism
-  for representing bound variables.  For
-  example in
-
-  @{ML_response_fake [display, gray]
-  "@{term \"\<lambda>x y. x y\"}"
-  "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 $}.
-
-  Isabelle makes a distinction between \emph{free} variables (term-constructor
-  @{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]
-"let
-  val v1 = Var ((\"x\", 3), @{typ bool})
-  val v2 = Var ((\"x1\", 3), @{typ bool})
-  val v3 = Free (\"x\", @{typ bool})
-in
-  string_of_terms @{context} [v1, v2, v3]
-  |> tracing
-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. 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
-  definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
-  For constructing terms involving HOL constants, many helper functions are defined
-  in @{ML_file "HOL/Tools/hologic.ML"}.
-  \end{readmore}
-  
-  Constructing terms via antiquotations has the advantage that only typable
-  terms can be constructed. For example
-
-  @{ML_response_fake_both [display,gray]
-  "@{term \"x x\"}"
-  "Type unification failed: Occurs check!"}
-
-  raises a typing error, while it perfectly ok to construct the term
-
-  @{ML_response_fake [display,gray] 
-"let
-  val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
-in 
-  tracing (string_of_term @{context} omega)
-end"
-  "x x"}
-
-  with the raw ML-constructors.
-  
-  Sometimes the internal representation of terms can be surprisingly different
-  from what you see at the user-level, because the layers of
-  parsing/type-checking/pretty printing can be quite elaborate. 
-
-  \begin{exercise}
-  Look at the internal term representation of the following terms, and
-  find out why they are represented like this:
-
-  \begin{itemize}
-  \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}  
-  \item @{term "\<lambda>(x,y). P y x"}  
-  \item @{term "{ [x::int] | x. x \<le> -2 }"}  
-  \end{itemize}
-
-  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 the following ML-function to set the printing depth to a higher 
-  value:
-
-  @{ML [display,gray] "print_depth 50"}
-  \end{exercise}
-
-  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\"})" 
-"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
- Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
- 
-  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>)"}
-
-  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:
-
-  @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
-
-  The corresponding datatype is
-*}
-  
-ML_val{*datatype typ =
-  Type  of string * typ list 
-| TFree of string * sort 
-| TVar  of indexname * sort *}
-
-text {*
-  Like with terms, there is the distinction between free type
-  variables (term-constructor @{ML "TFree"} and schematic
-  type variables (term-constructor @{ML "TVar"}). A type constant,
-  like @{typ "int"} or @{typ bool}, are types with an empty list
-  of argument types. However, it is a bit difficult to show an
-  example, because Isabelle always pretty-prints types (unlike terms).
-  Here is a contrived example:
-
-  @{ML_response [display, gray]
-  "if Type (\"bool\", []) = @{typ \"bool\"} then true else false"
-  "true"}
-
-  \begin{readmore}
-  Types are described in detail in \isccite{sec:types}. Their
-  definition and many useful operations are implemented 
-  in @{ML_file "Pure/type.ML"}.
-  \end{readmore}
-*}
-
-section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
-
-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
-  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:
-
-*}
-
-ML{*fun make_imp P Q =
-let
-  val x = Free ("x", @{typ nat})
-in 
-  Logic.all x (Logic.mk_implies (P $ x, Q $ x))
-end *}
-
-text {*
-  The reason is that you cannot pass the arguments @{term P} and @{term Q} 
-  into an antiquotation.\footnote{At least not at the moment.} For example 
-  the following does \emph{not} work.
-*}
-
-ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
-
-text {*
-  To see this, apply @{text "@{term S}"} and @{text "@{term T}"} 
-  to both functions. With @{ML make_imp} you obtain the intended term involving 
-  the given arguments
-
-  @{ML_response [display,gray] "make_imp @{term S} @{term T}" 
-"Const \<dots> $ 
-  Abs (\"x\", Type (\"nat\",[]),
-    Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
-
-  whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 
-  and @{text "Q"} from the antiquotation.
-
-  @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" 
-"Const \<dots> $ 
-  Abs (\"x\", \<dots>,
-    Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
-                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
-
-  There are a number of handy functions that are frequently used for 
-  constructing terms. One is the function @{ML_ind  list_comb}, which takes a term
-  and a list of terms as arguments, and produces as output the term
-  list applied to the term. For example
-
-@{ML_response_fake [display,gray]
-"let
-  val trm = @{term \"P::nat\"}
-  val args = [@{term \"True\"}, @{term \"False\"}]
-in
-  list_comb (trm, args)
-end"
-"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
-
-  Another handy function is @{ML_ind  lambda}, which abstracts a variable 
-  in a term. For example
-
-  @{ML_response_fake [display,gray]
-"let
-  val x_nat = @{term \"x::nat\"}
-  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
-in
-  lambda x_nat trm
-end"
-  "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
-
-  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
-  and an abstraction. It also records the type of the abstracted
-  variable and for printing purposes also its name.  Note that because of the
-  typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
-  is of the same type as the abstracted variable. If it is of different type,
-  as in
-
-  @{ML_response_fake [display,gray]
-"let
-  val x_int = @{term \"x::int\"}
-  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
-in
-  lambda x_int trm
-end"
-  "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
-
-  then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 
-  This is a fundamental principle
-  of Church-style typing, where variables with the same name still differ, if they 
-  have different type.
-
-  There is also the function @{ML_ind  subst_free} with which terms can be
-  replaced by other terms. For example below, we will replace in @{term
-  "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
-  @{term y}, and @{term x} by @{term True}.
-
-  @{ML_response_fake [display,gray]
-"let
-  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 [sub1, sub2] trm
-end"
-  "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
-
-  As can be seen, @{ML subst_free} does not take typability into account.
-  However it takes alpha-equivalence into account:
-
-  @{ML_response_fake [display, gray]
-"let
-  val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
-  val trm = @{term \"(\<lambda>x::nat. x)\"}
-in
-  subst_free [sub] trm
-end"
-  "Free (\"x\", \"nat\")"}
-
-  Similarly the function @{ML_ind  subst_bounds}, replaces lose bound 
-  variables with terms. To see how this function works, let us implement a
-  function that strips off the outermost quantifiers in a term.
-*}
-
-ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
-         strip_alls t |>> cons (Free (n, T))
-  | strip_alls t = ([], t) *}
-
-text {*
-  The function returns a pair consisting of the stripped off variables and
-  the body of the universal quantifications. For example
-
-  @{ML_response_fake [display, gray]
-  "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
-"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
-  Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
-
-  After calling @{ML strip_alls}, you obtain a term with lose bound variables. With
-  the function @{ML subst_bounds}, you can replace these lose @{ML_ind 
-  Bound}s with the stripped off variables.
-
-  @{ML_response_fake [display, gray, linenos]
-  "let
-  val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
-in 
-  subst_bounds (rev vrs, trm) 
-  |> string_of_term @{context}
-  |> tracing
-end"
-  "x = y"}
-
-  Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls}
-  returned. The reason is that the head of the list the function @{ML subst_bounds}
-  takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}
-  and so on. 
-
-  There are many convenient functions that construct specific HOL-terms. For
-  example @{ML_ind  mk_eq in HOLogic} constructs an equality out of two terms.
-  The types needed in this equality are calculated from the type of the
-  arguments. For example
-
-@{ML_response_fake [gray,display]
-"let
-  val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
-in
-  string_of_term @{context} eq
-  |> tracing
-end"
-  "True = False"}
-*}
-
-text {*
-  \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}
-
-  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
-  @{text is_true} as follows
-*}
-
-ML{*fun is_true @{term True} = true
-  | is_true _ = false*}
-
-text {*
-  this does not work for picking out @{text "\<forall>"}-quantified terms. Because
-  the function 
-*}
-
-ML{*fun is_all (@{term All} $ _) = true
-  | is_all _ = false*}
-
-text {* 
-  will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: 
-
-  @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
-
-  The problem is that the @{text "@term"}-antiquotation in the pattern 
-  fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
-  an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
-  for this function is
-*}
-
-ML{*fun is_all (Const ("All", _) $ _) = true
-  | is_all _ = false*}
-
-text {* 
-  because now
-
-@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
-
-  matches correctly (the first wildcard in the pattern matches any type and the
-  second any term).
-
-  However there is still a problem: consider the similar function that
-  attempts to pick out @{text "Nil"}-terms:
-*}
-
-ML{*fun is_nil (Const ("Nil", _)) = true
-  | is_nil _ = false *}
-
-text {* 
-  Unfortunately, also this function does \emph{not} work as expected, since
-
-  @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
-
-  The problem is that on the ML-level the name of a constant is more
-  subtle than you might expect. The function @{ML is_all} worked correctly,
-  because @{term "All"} is such a fundamental constant, which can be referenced
-  by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
-
-  @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
-
-  the name of the constant @{text "Nil"} depends on the theory in which the
-  term constructor is defined (@{text "List"}) and also in which datatype
-  (@{text "list"}). Even worse, some constants have a name involving
-  type-classes. Consider for example the constants for @{term "zero"} and
-  \mbox{@{text "(op *)"}}:
-
-  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
- "(Const (\"HOL.zero_class.zero\", \<dots>), 
- Const (\"HOL.times_class.times\", \<dots>))"}
-
-  While you could use the complete name, for example 
-  @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
-  matching against @{text "Nil"}, this would make the code rather brittle. 
-  The reason is that the theory and the name of the datatype can easily change. 
-  To make the code more robust, it is better to use the antiquotation 
-  @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
-  variable parts of the constant's name. Therefore a function for 
-  matching against constants that have a polymorphic type should 
-  be written as follows.
-*}
-
-ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
-  | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
-  | is_nil_or_all _ = false *}
-
-text {*
-  The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
-  For example
-
-  @{ML_response [display,gray]
-  "@{type_name \"list\"}" "\"List.list\""}
-
-  (FIXME: Explain the following better.)
-
-  Occasionally you have to calculate what the ``base'' name of a given
-  constant is. For this you can use the function @{ML_ind  "Sign.extern_const"} or
-  @{ML_ind  Long_Name.base_name}. For example:
-
-  @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
-
-  The difference between both functions is that @{ML extern_const in Sign} returns
-  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
-  strips off all qualifiers.
-
-  \begin{readmore}
-  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
-  functions about signatures in @{ML_file "Pure/sign.ML"}.
-  \end{readmore}
-
-  Although types of terms can often be inferred, there are many
-  situations where you need to construct types manually, especially  
-  when defining constants. For example the function returning a function 
-  type is as follows:
-
-*} 
-
-ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
-
-text {* This can be equally written with the combinator @{ML_ind  "-->"} as: *}
-
-ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
-
-text {*
-  If you want to construct a function type with more than one argument
-  type, then you can use @{ML_ind  "--->"}.
-*}
-
-ML{*fun make_fun_types tys ty = tys ---> ty *}
-
-text {*
-  A handy function for manipulating terms is @{ML_ind  map_types}: it takes a 
-  function and applies it to every type in a term. You can, for example,
-  change every @{typ nat} in a term into an @{typ int} using the function:
-*}
-
-ML{*fun nat_to_int ty =
-  (case ty of
-     @{typ nat} => @{typ int}
-   | Type (s, tys) => Type (s, map nat_to_int tys)
-   | _ => ty)*}
-
-text {*
-  Here is an example:
-
-@{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\")"}
-
-  If you want to obtain the list of free type-variables of a term, you
-  can use the function @{ML_ind  add_tfrees in Term} 
-  (similarly @{ML_ind  add_tvars in Term} for the schematic type-variables). 
-  One would expect that such functions
-  take a term as input and return a list of types. But their type is actually 
-
-  @{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}
-
-  that is they take, besides a term, also a list of type-variables as input. 
-  So in order to obtain the list of type-variables of a term you have to 
-  call them as follows
-
-  @{ML_response [gray,display]
-  "Term.add_tfrees @{term \"(a, b)\"} []"
-  "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
-
-  The reason for this definition is that @{ML add_tfrees in Term} can
-  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}
-*}
-
-
-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. 
-  Given a well-typed term, the function @{ML_ind  type_of} returns the 
-  type of a term. Consider for example:
-
-  @{ML_response [display,gray] 
-  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
-
-  To calculate the type, this function traverses the whole term and will
-  detect any typing inconsistency. For example changing the type of the variable 
-  @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 
-
-  @{ML_response_fake [display,gray] 
-  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 
-  "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
-
-  Since the complete traversal might sometimes be too costly and
-  not necessary, there is the function @{ML_ind  fastype_of}, which 
-  also returns the type of a term.
-
-  @{ML_response [display,gray] 
-  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
-
-  However, efficiency is gained on the expense of skipping some tests. You 
-  can see this in the following example
-
-   @{ML_response [display,gray] 
-  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
-
-  where no error is detected.
-
-  Sometimes it is a bit inconvenient to construct a term with 
-  complete typing annotations, especially in cases where the typing 
-  information is redundant. A short-cut is to use the ``place-holder'' 
-  type @{ML_ind  dummyT} and then let type-inference figure out the 
-  complete type. An example is as follows:
-
-  @{ML_response_fake [display,gray] 
-"let
-  val c = Const (@{const_name \"plus\"}, dummyT) 
-  val o = @{term \"1::nat\"} 
-  val v = Free (\"x\", dummyT)
-in   
-  Syntax.check_term @{context} (c $ o $ v)
-end"
-"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
-  Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
-
-  Instead of giving explicitly the type for the constant @{text "plus"} and the free 
-  variable @{text "x"}, type-inference fills in the missing information.
-
-  \begin{readmore}
-  See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
-  checking and pretty-printing of terms are defined. Functions related to
-  type-inference are implemented in @{ML_file "Pure/type.ML"} and 
-  @{ML_file "Pure/type_infer.ML"}. 
-  \end{readmore}
-
-  (FIXME: say something about sorts)
-
-  \begin{exercise}
-  Check that the function defined in Exercise~\ref{fun:revsum} returns a
-  result that type-checks. See what happens to the  solutions of this 
-  exercise given in \ref{ch:solutions} when they receive an ill-typed term
-  as input.
-  \end{exercise}
-*}
-
-
-section {* Theorems *}
-
-text {*
-  Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
-  that can only be built by going through interfaces. As a consequence, every proof 
-  in Isabelle is correct by construction. This follows the tradition of the LCF approach
-  \cite{GordonMilnerWadsworth79}.
-
-
-  To see theorems in ``action'', let us give a proof on the ML-level for the following 
-  statement:
-*}
-
-  lemma 
-   assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
-   and     assm\<^isub>2: "P t"
-   shows "Q t" (*<*)oops(*>*) 
-
-text {*
-  The corresponding ML-code is as follows:
-
-@{ML_response_fake [display,gray]
-"let
-  val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
-  val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}
-
-  val Pt_implies_Qt = 
-        assume assm1
-        |> forall_elim @{cterm \"t::nat\"};
-  
-  val Qt = implies_elim Pt_implies_Qt (assume assm2);
-in
-  Qt 
-  |> implies_intr assm2
-  |> implies_intr assm1
-end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
-
-  This code-snippet constructs the following proof:
-
-  \[
-  \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
-    {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
-       {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
-          {\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
-                 {\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
-                 &
-           \infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
-          }
-       }
-    }
-  \]
-
-  However, while we obtained a theorem as result, this theorem is not
-  yet stored in Isabelle's theorem database. So it cannot be referenced later
-  on. How to store theorems will be explained in Section~\ref{sec:storing}.
-
-  \begin{readmore}
-  For the functions @{text "assume"}, @{text "forall_elim"} etc 
-  see \isccite{sec:thms}. The basic functions for theorems are defined in
-  @{ML_file "Pure/thm.ML"}. 
-  \end{readmore}
-
-  (FIXME: handy functions working on theorems, like @{ML_ind  rulify in ObjectLogic} and so on) 
-
-  (FIXME: how to add case-names to goal states - maybe in the 
-  next section)
-
-  (FIXME: example for how to add theorem styles)
-*}
-
-ML {*
-fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) =
-      strip_assums_all ((a, T)::params, t)
-  | strip_assums_all (params, B) = (params, B)
-
-fun style_parm_premise i ctxt t =
-  let val prems = Logic.strip_imp_prems t in
-    if i <= length prems
-    then let val (params,t) = strip_assums_all([], nth prems (i - 1))
-         in subst_bounds(map Free params, t) end
-    else error ("Not enough premises for prem" ^ string_of_int i ^
-      " in propositon: " ^ string_of_term ctxt t)
-  end;
-*}
-
-ML {*
-strip_assums_all ([], @{term "\<And>x y. A x y"})
-*}
-
-setup %gray {*
-  TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
-  TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
-*}
-
-
-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 {*
-  Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
-  "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
-  annotated to theorems, but functions that do further processing once a
-  theorem is proved. In particular, it is not possible to find out
-  what are all theorems that have a given attribute in common, unless of course
-  the function behind the attribute stores the theorems in a retrievable 
-  data structure. 
-
-  If you want to print out all currently known attributes a theorem can have, 
-  you can use the Isabelle command
-
-  \begin{isabelle}
-  \isacommand{print\_attributes}\\
-  @{text "> COMP:  direct composition with rules (no lifting)"}\\
-  @{text "> HOL.dest:  declaration of Classical destruction rule"}\\
-  @{text "> HOL.elim:  declaration of Classical elimination rule"}\\
-  @{text "> \<dots>"}
-  \end{isabelle}
-  
-  The theorem attributes fall roughly into two categories: the first category manipulates
-  the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
-  stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds
-  the theorem to the current simpset).
-
-  To explain how to write your own attribute, let us start with an extremely simple 
-  version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
-  to produce the ``symmetric'' version of an equation. The main function behind 
-  this attribute is
-*}
-
-ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
-
-text {* 
-  where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 
-  context (which we ignore in the code above) and a theorem (@{text thm}), and 
-  returns another theorem (namely @{text thm} resolved with the theorem 
-  @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind "RS"} 
-  is explained in Section~\ref{sec:simpletacs}). The function 
-  @{ML rule_attribute in Thm} then returns  an attribute.
-
-  Before we can use the attribute, we need to set it up. This can be done
-  using the Isabelle command \isacommand{attribute\_setup} as follows:
-*}
-
-attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *} 
-  "applying the sym rule"
-
-text {*
-  Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
-  for the theorem attribute. Since the attribute does not expect any further 
-  arguments (unlike @{text "[THEN \<dots>]"}, for example), we use the parser @{ML
-  Scan.succeed}. Later on we will also consider attributes taking further
-  arguments. An example for the attribute @{text "[my_sym]"} is the proof
-*} 
-
-lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
-
-text {*
-  which stores the theorem @{thm test} under the name @{thm [source] test}. You
-  can see this, if you query the lemma: 
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "test"}\\
-  @{text "> "}~@{thm test}
-  \end{isabelle}
-
-  We can also use the attribute when referring to this theorem:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "test[my_sym]"}\\
-  @{text "> "}~@{thm test[my_sym]}
-  \end{isabelle}
-
-  An alternative for setting up an attribute is the function @{ML_ind  setup in Attrib}.
-  So instead of using \isacommand{attribute\_setup}, you can also set up the
-  attribute as follows:
-*}
-
-ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
-  "applying the sym rule" *}
-
-text {*
-  This gives a function from @{ML_type "Context.theory -> Context.theory"}, which
-  can be used for example with \isacommand{setup}.
-
-  As an example of a slightly more complicated theorem attribute, we implement 
-  our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
-  as argument and resolve the proved theorem with this list (one theorem 
-  after another). The code for this attribute is
-*}
-
-ML{*fun MY_THEN thms = 
-  Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
-
-text {* 
-  where @{ML swap} swaps the components of a pair. The setup of this theorem
-  attribute uses the parser @{ML thms in Attrib}, which parses a list of
-  theorems. 
-*}
-
-attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} 
-  "resolving the list of theorems with the proved theorem"
-
-text {* 
-  You can, for example, use this theorem attribute to turn an equation into a 
-  meta-equation:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\
-  @{text "> "}~@{thm test[MY_THEN eq_reflection]}
-  \end{isabelle}
-
-  If you need the symmetric version as a meta-equation, you can write
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\
-  @{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
-  \end{isabelle}
-
-  It is also possible to combine different theorem attributes, as in:
-  
-  \begin{isabelle}
-  \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
-  @{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
-  \end{isabelle}
-  
-  However, here also a weakness of the concept
-  of theorem attributes shows through: since theorem attributes can be
-  arbitrary functions, they do not in general commute. If you try
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
-  @{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
-  \end{isabelle}
-
-  you get an exception indicating that the theorem @{thm [source] sym}
-  does not resolve with meta-equations. 
-
-  The purpose of @{ML_ind  rule_attribute in Thm} is to directly manipulate theorems.
-  Another usage of theorem attributes is to add and delete theorems from stored data.
-  For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
-  current simpset. For these applications, you can use @{ML_ind  declaration_attribute in Thm}. 
-  To illustrate this function, let us introduce a reference containing a list
-  of theorems.
-*}
-
-ML{*val my_thms = ref ([] : thm list)*}
-
-text {* 
-  The purpose of this reference is to store a list of theorems.
-  We are going to modify it by adding and deleting theorems.
-  However, a word of warning: such references must not 
-  be used in any code that is meant to be more than just for testing purposes! 
-  Here it is only used to illustrate matters. We will show later how to store 
-  data properly without using references.
- 
-  We need to provide two functions that add and delete theorems from this list. 
-  For this we use the two functions:
-*}
-
-ML{*fun my_thm_add thm ctxt =
-  (my_thms := Thm.add_thm thm (!my_thms); ctxt)
-
-fun my_thm_del thm ctxt =
-  (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
-
-text {*
-  These functions take a theorem and a context and, for what we are explaining
-  here it is sufficient that they just return the context unchanged. They change
-  however the reference @{ML my_thms}, whereby the function 
-  @{ML_ind  add_thm in Thm} adds a theorem if it is not already included in 
-  the list, and @{ML_ind  del_thm in Thm} deletes one (both functions use the 
-  predicate @{ML_ind  eq_thm_prop in Thm}, which compares theorems according to 
-  their proved propositions modulo alpha-equivalence).
-
-  You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into 
-  attributes with the code
-*}
-
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
-
-text {* 
-  and set up the attributes as follows
-*}
-
-attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} 
-  "maintaining a list of my_thms - rough test only!" 
-
-text {*
-  The parser @{ML_ind  add_del in Attrib} is a predefined parser for 
-  adding and deleting lemmas. Now if you prove the next lemma 
-  and attach to it the attribute @{text "[my_thms]"}
-*}
-
-lemma trueI_2[my_thms]: "True" by simp
-
-text {*
-  then you can see it is added to the initially empty list.
-
-  @{ML_response_fake [display,gray]
-  "!my_thms" "[\"True\"]"}
-
-  You can also add theorems using the command \isacommand{declare}.
-*}
-
-declare test[my_thms] trueI_2[my_thms add] 
-
-text {*
-  With this attribute, the @{text "add"} operation is the default and does 
-  not need to be explicitly given. These three declarations will cause the 
-  theorem list to be updated as:
-
-  @{ML_response_fake [display,gray]
-  "!my_thms"
-  "[\"True\", \"Suc (Suc 0) = 2\"]"}
-
-  The theorem @{thm [source] trueI_2} only appears once, since the 
-  function @{ML_ind  add_thm in Thm} tests for duplicates, before extending
-  the list. Deletion from the list works as follows:
-*}
-
-declare test[my_thms del]
-
-text {* After this, the theorem list is again: 
-
-  @{ML_response_fake [display,gray]
-  "!my_thms"
-  "[\"True\"]"}
-
-  We used in this example two functions declared as @{ML_ind  declaration_attribute in Thm}, 
-  but there can be any number of them. We just have to change the parser for reading
-  the arguments accordingly. 
-
-  However, as said at the beginning of this example, using references for storing theorems is
-  \emph{not} the received way of doing such things. The received way is to 
-  start a ``data slot'', below called @{text MyThmsData}, generated by the functor 
-  @{text GenericDataFun}:
-*}
-
-ML{*structure MyThmsData = GenericDataFun
- (type T = thm list
-  val empty = []
-  val extend = I
-  fun merge _ = Thm.merge_thms) *}
-
-text {*
-  The type @{text "T"} of this data slot is @{ML_type "thm list"}.\footnote{FIXME: give a pointer
-  to where data slots are explained properly.}
-  To use this data slot, you only have to change @{ML my_thm_add} and
-  @{ML my_thm_del} to:
-*}
-
-ML{*val my_thm_add = MyThmsData.map o Thm.add_thm
-val my_thm_del = MyThmsData.map o Thm.del_thm*}
-
-text {*
-  where @{ML MyThmsData.map} updates the data appropriately. The
-  corresponding theorem attributes are
-*}
-
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
-
-text {*
-  and the setup is as follows
-*}
-
-attribute_setup %gray my_thms2 = {* Attrib.add_del my_add my_del *} 
-  "properly maintaining a list of my_thms"
-
-text {*
-  Initially, the data slot is empty 
-
-  @{ML_response_fake [display,gray]
-  "MyThmsData.get (Context.Proof @{context})"
-  "[]"}
-
-  but if you prove
-*}
-
-lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
-
-text {*
-  then the lemma is recorded. 
-
-  @{ML_response_fake [display,gray]
-  "MyThmsData.get (Context.Proof @{context})"
-  "[\"3 = Suc (Suc (Suc 0))\"]"}
-
-  With theorem attribute @{text my_thms2} you can also nicely see why it 
-  is important to 
-  store data in a ``data slot'' and \emph{not} in a reference. Backtrack
-  to the point just before the lemma @{thm [source] three} was proved and 
-  check the the content of @{ML_struct MyThmsData}: it should be empty. 
-  The addition has been properly retracted. Now consider the proof:
-*}
-
-lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
-
-text {*
-  Checking the content of @{ML my_thms} gives
-
-  @{ML_response_fake [display,gray]
-  "!my_thms"
-  "[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
-
-  as expected, but if you backtrack before the lemma @{thm [source] four}, the
-  content of @{ML my_thms} is unchanged. The backtracking mechanism
-  of Isabelle is completely oblivious about what to do with references, but
-  properly treats ``data slots''!
-
-  Since storing theorems in a list is such a common task, there is the special
-  functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain
-  a named theorem list, you just declare
-*}
-
-ML{*structure FooRules = Named_Thms
- (val name = "foo" 
-  val description = "Rules for foo") *}
-
-text {*
-  and set up the @{ML_struct FooRules} with the command
-*}
-
-setup %gray {* FooRules.setup *}
-
-text {*
-  This code declares a data slot where the theorems are stored,
-  an attribute @{text foo} (with the @{text add} and @{text del} options
-  for adding and deleting theorems) and an internal ML interface to retrieve and 
-  modify the theorems.
-
-  Furthermore, the facts are made available on the user-level under the dynamic 
-  fact name @{text foo}. For example you can declare three lemmas to be of the kind
-  @{text foo} by:
-*}
-
-lemma rule1[foo]: "A" sorry
-lemma rule2[foo]: "B" sorry
-lemma rule3[foo]: "C" sorry
-
-text {* and undeclare the first one by: *}
-
-declare rule1[foo del]
-
-text {* and query the remaining ones with:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "foo"}\\
-  @{text "> ?C"}\\
-  @{text "> ?B"}
-  \end{isabelle}
-
-  On the ML-level the rules marked with @{text "foo"} can be retrieved
-  using the function @{ML FooRules.get}:
-
-  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
-
-  \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
-  \end{readmore}
-
-  (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
-
-
-  \begin{readmore}
-  FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in 
-  @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
-  parsing.
-  \end{readmore}
-*}
-
-
-
-section {* Theories, Contexts and Local Theories (TBD) *}
-
-text {*
-  There are theories, proof contexts and local theories (in this order, if you
-  want to order them). 
-
-  In contrast to an ordinary theory, which simply consists of a type
-  signature, as well as tables for constants, axioms and theorems, a local
-  theory contains additional context information, such as locally fixed
-  variables and local assumptions that may be used by the package. The type
-  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
-  @{ML_type "Proof.context"}, although not every proof context constitutes a
-  valid local theory.
-*}
-
-(*
-ML{*signature UNIVERSAL_TYPE =
-sig
-  type t
-
-  val embed: unit -> ('a -> t) * (t -> 'a option)
-end*}
-
-ML{*structure U:> UNIVERSAL_TYPE =
-   struct
-      type t = exn
-
-      fun 'a embed () =
-         let
-            exception E of 'a
-            fun project (e: t): 'a option =
-               case e of
-                  E a => SOME a
-                | _ => NONE
-         in
-            (E, project)
-         end
-   end*}
-
-text {*
-  The idea is that type t is the universal type and that each call to embed
-  returns a new pair of functions (inject, project), where inject embeds a
-  value into the universal type and project extracts the value from the
-  universal type. A pair (inject, project) returned by embed works together in
-  that project u will return SOME v if and only if u was created by inject
-  v. If u was created by a different function inject', then project returns
-  NONE.
-
-  in library.ML
-*}
-
-ML_val{*structure Object = struct type T = exn end; *}
-
-ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
-   struct
-      val (intIn: int -> U.t, intOut) = U.embed ()
-      val r: U.t ref = ref (intIn 13)
-      val s1 =
-         case intOut (!r) of
-            NONE => "NONE"
-          | SOME i => Int.toString i
-      val (realIn: real -> U.t, realOut) = U.embed ()
-      val () = r := realIn 13.0
-      val s2 =
-         case intOut (!r) of
-            NONE => "NONE"
-          | SOME i => Int.toString i
-      val s3 =
-         case realOut (!r) of
-            NONE => "NONE"
-          | SOME x => Real.toString x
-      val () = tracing (concat [s1, " ", s2, " ", s3, "\n"])
-   end*}
-
-ML_val{*structure t = Test(U) *} 
-
-ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
-
-ML {* LocalTheory.restore *}
-ML {* LocalTheory.set_group *}
-*)
-
-section {* Storing Theorems\label{sec:storing} (TBD) *}
-
-text {* @{ML_ind  add_thms_dynamic in PureThy} *}
-
-local_setup %gray {* 
-  LocalTheory.note Thm.theoremK 
-    ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
-
-
-(* FIXME: some code below *)
-
-(*<*)
-(*
-setup {*
- Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
-*}
-*)
-lemma "bar = (1::nat)"
-  oops
-
-(*
-setup {*   
-  Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
- #> PureThy.add_defs false [((@{binding "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
-*)
-(*>*)
-
-section {* Pretty-Printing\label{sec:pretty} *}
-
-text {*
-  So far we printed out only plain strings without any formatting except for
-  occasional explicit line breaks using @{text [quotes] "\\n"}. This is
-  sufficient for ``quick-and-dirty'' printouts. For something more
-  sophisticated, Isabelle includes an infrastructure for properly formatting text.
-  This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
-  its functions do not operate on @{ML_type string}s, but on instances of the
-  type:
-
-  @{ML_type_ind [display, gray] "Pretty.T"}
-
-  The function @{ML str in Pretty} transforms a (plain) string into such a pretty 
-  type. For example
-
-  @{ML_response_fake [display,gray]
-  "Pretty.str \"test\"" "String (\"test\", 4)"}
-
-  where the result indicates that we transformed a string with length 4. Once
-  you have a pretty type, you can, for example, control where linebreaks may
-  occur in case the text wraps over a line, or with how much indentation a
-  text should be printed.  However, if you want to actually output the
-  formatted text, you have to transform the pretty type back into a @{ML_type
-  string}. This can be done with the function @{ML_ind  string_of in Pretty}. In what
-  follows we will use the following wrapper function for printing a pretty
-  type:
-*}
-
-ML{*fun pprint prt = tracing (Pretty.string_of prt)*}
-
-text {*
-  The point of the pretty-printing infrastructure is to give hints about how to
-  layout text and let Isabelle do the actual layout. Let us first explain
-  how you can insert places where a line break can occur. For this assume the
-  following function that replicates a string n times:
-*}
-
-ML{*fun rep n str = implode (replicate n str) *}
-
-text {*
-  and suppose we want to print out the string:
-*}
-
-ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
-
-text {*
-  We deliberately chose a large string so that it spans over more than one line. 
-  If we print out the string using the usual ``quick-and-dirty'' method, then
-  we obtain the ugly output:
-
-@{ML_response_fake [display,gray]
-"tracing test_str"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
-ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
-aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
-oooooooooooooobaaaaaaaaaaaar"}
-
-  We obtain the same if we just use
-
-@{ML_response_fake [display,gray]
-"pprint (Pretty.str test_str)"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
-ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
-aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
-oooooooooooooobaaaaaaaaaaaar"}
-
-  However by using pretty types you have the ability to indicate a possible
-  line break for example at each space. You can achieve this with the function
-  @{ML_ind  breaks in Pretty}, which expects a list of pretty types and inserts a
-  possible line break in between every two elements in this list. To print
-  this list of pretty types as a single string, we concatenate them 
-  with the function @{ML_ind  blk in Pretty} as follows:
-
-
-@{ML_response_fake [display,gray]
-"let
-  val ptrs = map Pretty.str (space_explode \" \" test_str)
-in
-  pprint (Pretty.blk (0, Pretty.breaks ptrs))
-end"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
-fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
-fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
-fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
-
-  Here the layout of @{ML test_str} is much more pleasing to the 
-  eye. The @{ML "0"} in @{ML_ind  blk in Pretty} stands for no indentation
-  of the printed string. You can increase the indentation and obtain
-  
-@{ML_response_fake [display,gray]
-"let
-  val ptrs = map Pretty.str (space_explode \" \" test_str)
-in
-  pprint (Pretty.blk (3, Pretty.breaks ptrs))
-end"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
-   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
-   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
-   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
-
-  where starting from the second line the indent is 3. If you want
-  that every line starts with the same indent, you can use the
-  function @{ML_ind  indent in Pretty} as follows:
-
-@{ML_response_fake [display,gray]
-"let
-  val ptrs = map Pretty.str (space_explode \" \" test_str)
-in
-  pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))
-end"
-"          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
-          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
-          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
-          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
-
-  If you want to print out a list of items separated by commas and 
-  have the linebreaks handled properly, you can use the function 
-  @{ML_ind  commas in Pretty}. For example
-
-@{ML_response_fake [display,gray]
-"let
-  val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
-in
-  pprint (Pretty.blk (0, Pretty.commas ptrs))
-end"
-"99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
-100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
-100016, 100017, 100018, 100019, 100020"}
-
-  where @{ML upto} generates a list of integers. You can print out this
-  list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
-  @{text [quotes] "}"}, and separated by commas using the function
-  @{ML_ind  enum in Pretty}. For example
-*}
-
-text {*
-  
-@{ML_response_fake [display,gray]
-"let
-  val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
-in
-  pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)
-end"
-"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
-  100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
-  100016, 100017, 100018, 100019, 100020}"}
-
-  As can be seen, this function prints out the ``set'' so that starting 
-  from the second, each new line as an indentation of 2.
-  
-  If you print out something that goes beyond the capabilities of the
-  standard functions, you can do relatively easily the formatting
-  yourself. Assume you want to print out a list of items where like in ``English''
-  the last two items are separated by @{text [quotes] "and"}. For this you can
-  write the function
-
-*}
-
-ML %linenosgray{*fun and_list [] = []
-  | and_list [x] = [x]
-  | and_list xs = 
-      let 
-        val (front, last) = split_last xs
-      in
-        (Pretty.commas front) @ 
-        [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]
-      end *}
-
-text {*
-  where Line 7 prints the beginning of the list and Line
-  8 the last item. We have to use @{ML "Pretty.brk 1"} in order
-  to insert a space (of length 1) before the 
-  @{text [quotes] "and"}. This space is also a place where a line break 
-  can occur. We do the same after the @{text [quotes] "and"}. This gives you
-  for example
-
-@{ML_response_fake [display,gray]
-"let
-  val ptrs = map (Pretty.str o string_of_int) (1 upto 22)
-in
-  pprint (Pretty.blk (0, and_list ptrs))
-end"
-"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
-and 22"}
-
-  Next we like to pretty-print a term and its type. For this we use the
-  function @{text "tell_type"}.
-*}
-
-ML %linenosgray{*fun tell_type ctxt t = 
-let
-  fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
-  val ptrm = Pretty.quote (Syntax.pretty_term ctxt t)
-  val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t))
-in
-  pprint (Pretty.blk (0, 
-    (pstr "The term " @ [ptrm] @ pstr " has type " 
-      @ [pty, Pretty.str "."])))
-end*}
-
-text {*
-  In Line 3 we define a function that inserts possible linebreaks in places
-  where a space is. In Lines 4 and 5 we pretty-print the term and its type
-  using the functions @{ML_ind  pretty_term in Syntax} and @{ML_ind 
-  pretty_typ in Syntax}. We also use the function @{ML_ind quote in
-  Pretty} in order to enclose the term and type inside quotation marks. In
-  Line 9 we add a period right after the type without the possibility of a
-  line break, because we do not want that a line break occurs there.
-
-
-  Now you can write
-
-  @{ML_response_fake [display,gray]
-  "tell_type @{context} @{term \"min (Suc 0)\"}"
-  "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
-  
-  To see the proper line breaking, you can try out the function on a bigger term 
-  and type. For example:
-
-  @{ML_response_fake [display,gray]
-  "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
-  "The term \"op = (op = (op = (op = (op = op =))))\" has type 
-\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
-
-
-  FIXME: TBD below
-*}
-
-ML {* pprint (Pretty.big_list "header"  (map (Pretty.str o string_of_int) (4 upto 10))) *}
-
-text {*
-chunks inserts forced breaks (unlike blk where you have to do this yourself)
-*}
-
-ML {* (Pretty.chunks [Pretty.str "a", Pretty.str "b"], 
-       Pretty.blk (0, [Pretty.str "a", Pretty.str "b"])) *}
-
-ML {*
-fun setmp_show_all_types f =
-   setmp show_all_types
-         (! show_types orelse ! show_sorts orelse ! show_all_types) f;
-
-val ctxt = @{context};
-val t1 = @{term "undefined::nat"};
-val t2 = @{term "Suc y"};
-val pty =        Pretty.block (Pretty.breaks
-             [(setmp show_question_marks false o setmp_show_all_types)
-                  (Syntax.pretty_term ctxt) t1,
-              Pretty.str "=", Syntax.pretty_term ctxt t2]);
-pty |> Pretty.string_of |> priority
-*}
-
-text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
-
-
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-
-
-ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-
-text {*
-  Still to be done:
-
-  What happens with big formulae?
-
-  \begin{readmore}
-  The general infrastructure for pretty-printing is implemented in the file
-  @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
-  contains pretty-printing functions for terms, types, theorems and so on.
-  
-  @{ML_file "Pure/General/markup.ML"}
-  \end{readmore}
-*}
-
-text {*
-  printing into the goal buffer as part of the proof state
-*}
-
-
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-
-text {* writing into the goal buffer *}
-
-ML {* fun my_hook interactive state =
-         (interactive ? Proof.goal_message (fn () => Pretty.str  
-"foo")) state
-*}
-
-setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
-
-lemma "False"
-oops
-
-
-section {* Misc (TBD) *}
-
-ML {*Datatype.get_info @{theory} "List.list"*}
-
-section {* Name Space Issues (TBD) *}
-
-
 end




