equal
deleted
inserted
replaced
1 theory Solutions |
1 theory Solutions |
2 imports Base "Recipes/Timing" |
2 imports Base "Recipes/Timing" |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
5 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
|
6 |
|
7 text {* \solution{ex:debruijn} *} |
|
8 |
|
9 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
|
10 |
|
11 fun rhs 1 = P 1 |
|
12 | rhs n = HOLogic.mk_conj (P n, rhs (n - 1)) |
|
13 |
|
14 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n) |
|
15 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
|
16 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
|
17 |
|
18 fun de_bruijn n = |
|
19 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*} |
6 |
20 |
7 text {* \solution{fun:revsum} *} |
21 text {* \solution{fun:revsum} *} |
8 |
22 |
9 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
23 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
10 p $ u $ rev_sum t |
24 p $ u $ rev_sum t |