--- 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}
*}