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 \ '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 \}"}). - 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 \}"}). 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 \}"} constructs terms of propositional type, - inserting the invisible @{text "Trueprop"}-coercions whenever necessary. + The antiquotation @{text "@{prop \}"} 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 \ Q x\"}, @{prop \"P x \ Q x\"})" - "(Const (\"==>\", \) $ \ $ \, Const (\"==>\", \) $ \ $ \)"} + "(Const (\"==>\", \) $ \ $ \, + Const (\"==>\", \) $ \ $ \)"} 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 \}"}. For example: @@ -1091,11 +1097,11 @@ @{ML_response_fake [display,gray] "let - val s1 = (@{term \"(f::nat \ nat \ nat) 0\"}, @{term \"y::nat \ nat\"}) - val s2 = (@{term \"x::nat\"}, @{term \"True\"}) + val sub1 = (@{term \"(f::nat \ nat \ nat) 0\"}, @{term \"y::nat \ nat\"}) + val sub2 = (@{term \"x::nat\"}, @{term \"True\"}) val trm = @{term \"((f::nat \ nat \ nat) 0) x\"} in - subst_free [s1, s2] trm + subst_free [sub1, sub2] trm end" "Free (\"y\", \"nat \ nat\") $ Const (\"True\", \"bool\")"} @@ -1104,10 +1110,10 @@ @{ML_response_fake [display, gray] "let - val s = (@{term \"(\y::nat. y)\"}, @{term \"x::nat\"}) + val sub = (@{term \"(\y::nat. y)\"}, @{term \"x::nat\"}) val trm = @{term \"(\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 + \ + t\<^isub>n"} (whereby @{text "n"} might be one) - and returns the reversed sum @{text "t\<^isub>n + \ + 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 \}"}. 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 + \ + t\<^isub>n"} (whereby @{text "n"} might be one) + and returns the reversed sum @{text "t\<^isub>n + \ + 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} *}