equal
deleted
inserted
replaced
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 |
6 |
|
7 text {* \solution{fun:revsum} *} |
|
8 |
|
9 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
|
10 p $ u $ rev_sum t |
|
11 | rev_sum t = t *} |
|
12 |
|
13 text {* |
|
14 An alternative solution using the function @{ML [index] mk_binop in HOLogic} is: |
|
15 *} |
|
16 |
|
17 ML{*fun rev_sum t = |
|
18 let |
|
19 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
|
20 | dest_sum u = [u] |
|
21 in |
|
22 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
|
23 end *} |
|
24 |
|
25 text {* \solution{fun:makesum} *} |
|
26 |
|
27 ML{*fun make_sum t1 t2 = |
|
28 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
|
29 |
7 text {* \solution{ex:debruijn} *} |
30 text {* \solution{ex:debruijn} *} |
8 |
31 |
9 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
32 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
10 |
33 |
11 fun rhs 1 = P 1 |
34 fun rhs 1 = P 1 |
15 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
38 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
16 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
39 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
17 |
40 |
18 fun de_bruijn n = |
41 fun de_bruijn n = |
19 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*} |
42 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*} |
20 |
|
21 text {* \solution{fun:revsum} *} |
|
22 |
|
23 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
|
24 p $ u $ rev_sum t |
|
25 | rev_sum t = t *} |
|
26 |
|
27 text {* |
|
28 An alternative solution using the function @{ML [index] mk_binop in HOLogic} is: |
|
29 *} |
|
30 |
|
31 ML{*fun rev_sum t = |
|
32 let |
|
33 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
|
34 | dest_sum u = [u] |
|
35 in |
|
36 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
|
37 end *} |
|
38 |
|
39 text {* \solution{fun:makesum} *} |
|
40 |
|
41 ML{*fun make_sum t1 t2 = |
|
42 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
|
43 |
43 |
44 text {* \solution{ex:scancmts} *} |
44 text {* \solution{ex:scancmts} *} |
45 |
45 |
46 ML{*val any = Scan.one (Symbol.not_eof) |
46 ML{*val any = Scan.one (Symbol.not_eof) |
47 |
47 |