70 but will be flagged as ill-formed when you try to typecheck or certify it |
70 but will be flagged as ill-formed when you try to typecheck or certify it |
71 (see Section~\ref{sec:typechecking}). Note that the names of bound variables |
71 (see Section~\ref{sec:typechecking}). Note that the names of bound variables |
72 are kept at abstractions for printing purposes, and so should be treated |
72 are kept at abstractions for printing purposes, and so should be treated |
73 only as ``comments''. Application in Isabelle is realised with the |
73 only as ``comments''. Application in Isabelle is realised with the |
74 term-constructor @{ML $}. |
74 term-constructor @{ML $}. |
|
75 |
|
76 Be careful if you pretty-print terms. Consider pretty-printing the abstraction |
|
77 term shown above: |
|
78 |
|
79 @{ML_response_fake [display, gray] |
|
80 "@{term \"\<lambda>x y. x y\"} |
|
81 |> pretty_term @{context} |
|
82 |> pwriteln" |
|
83 "\<lambda>x. x"} |
|
84 |
|
85 This is one common source for puzzlement in Isabelle, which has |
|
86 tacitly eta-contracted the output. You obtain a similar result |
|
87 with beta-redexes |
|
88 |
|
89 @{ML_response_fake [display, gray] |
|
90 "@{term \"(\<lambda>x y. x) 1 2\"} |
|
91 |> pretty_term @{context} |
|
92 |> pwriteln" |
|
93 "1"} |
|
94 |
|
95 There is a configuration value to switch off the tacit eta-contraction (see |
|
96 \ref{sec:printing}), but none for beta-contraction. So in certain cases you |
|
97 might have to inspect the internal representation of a term, instead of |
|
98 pretty printing it. Because of the alluded puzzlement that might arise from |
|
99 this feature of Isabelle, it is certainly an acrane fact that you should |
|
100 keep in mind about pretty-printing terms. |
75 |
101 |
76 Isabelle makes a distinction between \emph{free} variables (term-constructor |
102 Isabelle makes a distinction between \emph{free} variables (term-constructor |
77 @{ML Free} and written on the user level in blue colour) and |
103 @{ML Free} and written on the user level in blue colour) and |
78 \emph{schematic} variables (term-constructor @{ML Var} and written with a |
104 \emph{schematic} variables (term-constructor @{ML Var} and written with a |
79 leading question mark). Consider the following two examples |
105 leading question mark). Consider the following two examples |
187 Using just the antiquotation @{text "@{typ \"bool\"}"} we only see |
213 Using just the antiquotation @{text "@{typ \"bool\"}"} we only see |
188 |
214 |
189 @{ML_response [display, gray] |
215 @{ML_response [display, gray] |
190 "@{typ \"bool\"}" |
216 "@{typ \"bool\"}" |
191 "bool"} |
217 "bool"} |
192 |
|
193 which is the pretty printed version of @{text "bool"}. However, in PolyML |
218 which is the pretty printed version of @{text "bool"}. However, in PolyML |
194 (version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the |
219 (version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the |
195 function below we mimic the behaviour of the usual pretty printer for |
220 function below we mimic the behaviour of the usual pretty printer for |
196 datatypes (it uses pretty-printing functions which will be explained in more |
221 datatypes (it uses pretty-printing functions which will be explained in more |
197 detail in Section~\ref{sec:pretty}). |
222 detail in Section~\ref{sec:pretty}). |
391 end" |
416 end" |
392 "Free (\"x\", \"nat\")"} |
417 "Free (\"x\", \"nat\")"} |
393 |
418 |
394 Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound |
419 Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound |
395 variables with terms. To see how this function works, let us implement a |
420 variables with terms. To see how this function works, let us implement a |
396 function that strips off the outermost quantifiers in a term. |
421 function that strips off the outermost forall quantifiers in a term. |
397 *} |
422 *} |
398 |
423 |
399 ML{*fun strip_alls t = |
424 ML{*fun strip_alls t = |
400 let |
425 let |
401 fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T)) |
426 fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T)) |
402 in |
427 in |
403 case t of |
428 case t of |
404 Const ("All", _) $ Abs body => aux body |
429 Const (@{const_name All}, _) $ Abs body => aux body |
405 | _ => ([], t) |
430 | _ => ([], t) |
406 end*} |
431 end*} |
407 |
432 |
408 text {* |
433 text {* |
409 The function returns a pair consisting of the stripped off variables and |
434 The function returns a pair consisting of the stripped off variables and |
412 @{ML_response_fake [display, gray] |
437 @{ML_response_fake [display, gray] |
413 "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}" |
438 "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}" |
414 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")], |
439 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")], |
415 Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"} |
440 Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"} |
416 |
441 |
417 After calling @{ML strip_alls}, you obtain a term with lose bound variables. With |
442 Note that we produced in the body two dangling de Bruijn indices. |
418 the function @{ML subst_bounds}, you can replace these lose @{ML_ind |
443 Later on we will also use the inverse function that |
419 Bound in Term}s with the stripped off variables. |
444 builds the quantification from a body and a list of (free) variables. |
|
445 *} |
|
446 |
|
447 ML{*fun build_alls ([], t) = t |
|
448 | build_alls (Free (x, T) :: vs, t) = |
|
449 Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) |
|
450 $ Abs (x, T, build_alls (vs, t))*} |
|
451 |
|
452 text {* |
|
453 As said above, after calling @{ML strip_alls}, you obtain a term with loose |
|
454 bound variables. With the function @{ML subst_bounds}, you can replace these |
|
455 loose @{ML_ind Bound in Term}s with the stripped off variables. |
420 |
456 |
421 @{ML_response_fake [display, gray, linenos] |
457 @{ML_response_fake [display, gray, linenos] |
422 "let |
458 "let |
423 val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"} |
459 val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"} |
424 in |
460 in |
435 |
471 |
436 Notice also that this function might introduce name clashes, since we |
472 Notice also that this function might introduce name clashes, since we |
437 substitute just a variable with the name recorded in an abstraction. This |
473 substitute just a variable with the name recorded in an abstraction. This |
438 name is by no means unique. If clashes need to be avoided, then we should |
474 name is by no means unique. If clashes need to be avoided, then we should |
439 use the function @{ML_ind dest_abs in Term}, which returns the body where |
475 use the function @{ML_ind dest_abs in Term}, which returns the body where |
440 the lose de Bruijn index is replaced by a unique free variable. For example |
476 the loose de Bruijn index is replaced by a unique free variable. For example |
441 |
477 |
442 |
478 |
443 @{ML_response_fake [display,gray] |
479 @{ML_response_fake [display,gray] |
444 "let |
480 "let |
445 val body = Bound 0 $ Free (\"x\", @{typ nat}) |
481 val body = Bound 0 $ Free (\"x\", @{typ nat}) |
446 in |
482 in |
447 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body) |
483 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body) |
448 end" |
484 end" |
449 "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"} |
485 "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"} |
|
486 |
|
487 Sometimes it is necessary to manipulate de Bruijn indices in terms directly. |
|
488 There are many functions to do this. We describe only two. The first, |
|
489 @{ML_ind incr_boundvars in Term}, increases by an integer the indices |
|
490 of the loose bound variables in a term. In the code below |
|
491 |
|
492 @{ML_response_fake [display,gray] |
|
493 "@{term \"\<forall>x y z u. z = u\"} |
|
494 |> strip_alls |
|
495 ||> incr_boundvars 2 |
|
496 |> build_alls |
|
497 |> pretty_term @{context} |
|
498 |> pwriteln" |
|
499 "\<forall>x y z u. x = y"} |
|
500 |
|
501 we first strip off the forall-quantified variables (thus creating two loose |
|
502 bound variables in the body); then we increase the indices of the loose |
|
503 bound variables by @{ML 2} and finally re-quantify the variables. As a |
|
504 result of @{ML incr_boundvars}, we obtain now a term that has the equation |
|
505 between the first two quantified variables. |
|
506 |
|
507 The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term |
|
508 contains a loose bound of a certain index. For example |
|
509 |
|
510 @{ML_response_fake [gray,display] |
|
511 "let |
|
512 val body = snd (strip_alls @{term \"\<forall>x y. x = (y::bool)\"}) |
|
513 in |
|
514 [loose_bvar1 (body, 0), |
|
515 loose_bvar1 (body, 1), |
|
516 loose_bvar1 (body, 2)] |
|
517 end" |
|
518 "[true, true, false]"} |
450 |
519 |
451 There are also many convenient functions that construct specific HOL-terms |
520 There are also many convenient functions that construct specific HOL-terms |
452 in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in |
521 in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in |
453 HOLogic} constructs an equality out of two terms. The types needed in this |
522 HOLogic} constructs an equality out of two terms. The types needed in this |
454 equality are calculated from the type of the arguments. For example |
523 equality are calculated from the type of the arguments. For example |
628 |
697 |
629 \begin{exercise}\label{fun:makesum} |
698 \begin{exercise}\label{fun:makesum} |
630 Write a function that takes two terms representing natural numbers |
699 Write a function that takes two terms representing natural numbers |
631 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
700 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
632 number representing their sum. |
701 number representing their sum. |
|
702 \end{exercise} |
|
703 |
|
704 \begin{exercise}\label{fun:killqnt} |
|
705 Write a function that removes trivial forall and exists quantifiers that do not |
|
706 quantify over any variables. For example the term @{term "\<forall>x y z. P x = P |
|
707 z"} should be transformed to @{term "\<forall>x z. P x = P z"}, deleting the |
|
708 quantification @{term "y"}. Hint: use the functions @{ML incr_boundvars} |
|
709 and @{ML loose_bvar1}. |
633 \end{exercise} |
710 \end{exercise} |
634 |
711 |
635 \begin{exercise}\label{fun:makelist} |
712 \begin{exercise}\label{fun:makelist} |
636 Write a function that takes an integer @{text i} and |
713 Write a function that takes an integer @{text i} and |
637 produces an Isabelle integer list from @{text 1} upto @{text i}, |
714 produces an Isabelle integer list from @{text 1} upto @{text i}, |