# HG changeset patch # User Christian Urban # Date 1308657196 -3600 # Node ID 7a558c5119b20840ad41d212068f19db081167c5 # Parent 00921ae66622b6721e5ad19c9faf9566f3da12c6 added an excercise originally by Jasmin Blanchette diff -r 00921ae66622 -r 7a558c5119b2 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Mon Jun 20 13:59:58 2011 +0100 +++ b/ProgTutorial/Essential.thy Tue Jun 21 12:53:16 2011 +0100 @@ -73,6 +73,32 @@ only as ``comments''. Application in Isabelle is realised with the term-constructor @{ML $}. + Be careful if you pretty-print terms. Consider pretty-printing the abstraction + term shown above: + + @{ML_response_fake [display, gray] +"@{term \"\x y. x y\"} + |> pretty_term @{context} + |> pwriteln" + "\x. x"} + + This is one common source for puzzlement in Isabelle, which has + tacitly eta-contracted the output. You obtain a similar result + with beta-redexes + + @{ML_response_fake [display, gray] +"@{term \"(\x y. x) 1 2\"} + |> pretty_term @{context} + |> pwriteln" + "1"} + + There is a configuration value to switch off the tacit eta-contraction (see + \ref{sec:printing}), but none for beta-contraction. So in certain cases you + might have to inspect the internal representation of a term, instead of + pretty printing it. Because of the alluded puzzlement that might arise from + this feature of Isabelle, it is certainly an acrane fact that you should + keep in mind about pretty-printing terms. + 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 @@ -189,7 +215,6 @@ @{ML_response [display, gray] "@{typ \"bool\"}" "bool"} - which is the pretty printed version of @{text "bool"}. However, in PolyML (version @{text "\"}5.3) it is easy to install your own pretty printer. With the function below we mimic the behaviour of the usual pretty printer for @@ -393,7 +418,7 @@ Similarly the function @{ML_ind subst_bounds in Term}, 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. + function that strips off the outermost forall quantifiers in a term. *} ML{*fun strip_alls t = @@ -401,7 +426,7 @@ fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T)) in case t of - Const ("All", _) $ Abs body => aux body + Const (@{const_name All}, _) $ Abs body => aux body | _ => ([], t) end*} @@ -414,9 +439,20 @@ "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")], Const (\"op =\", \) $ 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 in Term}s with the stripped off variables. + Note that we produced in the body two dangling de Bruijn indices. + Later on we will also use the inverse function that + builds the quantification from a body and a list of (free) variables. +*} + +ML{*fun build_alls ([], t) = t + | build_alls (Free (x, T) :: vs, t) = + Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) + $ Abs (x, T, build_alls (vs, t))*} + +text {* + As said above, after calling @{ML strip_alls}, you obtain a term with loose + bound variables. With the function @{ML subst_bounds}, you can replace these + loose @{ML_ind Bound in Term}s with the stripped off variables. @{ML_response_fake [display, gray, linenos] "let @@ -437,7 +473,7 @@ substitute just a variable with the name recorded in an abstraction. This name is by no means unique. If clashes need to be avoided, then we should use the function @{ML_ind dest_abs in Term}, which returns the body where - the lose de Bruijn index is replaced by a unique free variable. For example + the loose de Bruijn index is replaced by a unique free variable. For example @{ML_response_fake [display,gray] @@ -448,6 +484,39 @@ end" "(\"xa\", Free (\"xa\", \"Nat.nat \ bool\") $ Free (\"x\", \"Nat.nat\"))"} + Sometimes it is necessary to manipulate de Bruijn indices in terms directly. + There are many functions to do this. We describe only two. The first, + @{ML_ind incr_boundvars in Term}, increases by an integer the indices + of the loose bound variables in a term. In the code below + +@{ML_response_fake [display,gray] +"@{term \"\x y z u. z = u\"} + |> strip_alls + ||> incr_boundvars 2 + |> build_alls + |> pretty_term @{context} + |> pwriteln" + "\x y z u. x = y"} + + we first strip off the forall-quantified variables (thus creating two loose + bound variables in the body); then we increase the indices of the loose + bound variables by @{ML 2} and finally re-quantify the variables. As a + result of @{ML incr_boundvars}, we obtain now a term that has the equation + between the first two quantified variables. + + The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term + contains a loose bound of a certain index. For example + + @{ML_response_fake [gray,display] +"let + val body = snd (strip_alls @{term \"\x y. x = (y::bool)\"}) +in + [loose_bvar1 (body, 0), + loose_bvar1 (body, 1), + loose_bvar1 (body, 2)] +end" + "[true, true, false]"} + There are also many convenient functions that construct specific HOL-terms in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in HOLogic} constructs an equality out of two terms. The types needed in this @@ -632,6 +701,14 @@ number representing their sum. \end{exercise} + \begin{exercise}\label{fun:killqnt} + Write a function that removes trivial forall and exists quantifiers that do not + quantify over any variables. For example the term @{term "\x y z. P x = P + z"} should be transformed to @{term "\x z. P x = P z"}, deleting the + quantification @{term "y"}. Hint: use the functions @{ML incr_boundvars} + and @{ML loose_bvar1}. + \end{exercise} + \begin{exercise}\label{fun:makelist} Write a function that takes an integer @{text i} and produces an Isabelle integer list from @{text 1} upto @{text i}, diff -r 00921ae66622 -r 7a558c5119b2 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Mon Jun 20 13:59:58 2011 +0100 +++ b/ProgTutorial/Intro.thy Tue Jun 21 12:53:16 2011 +0100 @@ -252,7 +252,8 @@ \ref{chp:package} describing this package and has been helpful \emph{beyond measure} with answering questions about Isabelle. - \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}. + \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty} + and exercise \ref{fun:killqnt}. \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} diff -r 00921ae66622 -r 7a558c5119b2 ProgTutorial/Solutions.thy --- a/ProgTutorial/Solutions.thy Mon Jun 20 13:59:58 2011 +0100 +++ b/ProgTutorial/Solutions.thy Tue Jun 21 12:53:16 2011 +0100 @@ -35,6 +35,43 @@ ML{*fun make_sum t1 t2 = HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} +text {* \solution{fun:killqnt} *} + +ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}] + +fun kill_trivial_quantifiers trm = +let + fun aux t = + case t of + Const (s1, T1) $ Abs (x, T2, t2) => + if member (op =) quantifiers s1 andalso not (loose_bvar1 (t2, 0)) + then incr_boundvars ~1 (aux t2) + else Const (s1, T1) $ Abs (x, T2, aux t2) + | t1 $ t2 => aux t1 $ aux t2 + | Abs (s, T, t') => Abs (s, T, aux t') + | _ => t +in + aux trm +end*} + +text {* + In line 7 we traverse the term, by first checking whether a term is an + application of a constant with an abstraction. If the constant stands for + a listed quantifier (see Line 1) and the bound variable does not occur + as a loose bound variable in the body, then we delete the quantifier. + For this we have to increase all other dangling de Bruijn indices by + @{text "-1"} to account for the deleted quantifier. An example is + as follows: + + @{ML_response_fake [display,gray] + "@{prop \"\x y z. P x = P z\"} + |> kill_trivial_quantifiers + |> pretty_term @{context} + |> pwriteln" + "\x z. P x = P z"} +*} + + text {* \solution{fun:makelist} *} diff -r 00921ae66622 -r 7a558c5119b2 progtutorial.pdf Binary file progtutorial.pdf has changed