6 |
6 |
7 text {* \solution{fun:revsum} *} |
7 text {* \solution{fun:revsum} *} |
8 |
8 |
9 ML{*fun rev_sum t = |
9 ML{*fun rev_sum t = |
10 let |
10 let |
11 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
11 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
12 | dest_sum u = [u] |
12 | dest_sum u = [u] |
13 in |
13 in |
14 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
14 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
15 end *} |
15 end *} |
16 |
16 |
17 text {* \solution{fun:makesum} *} |
17 text {* \solution{fun:makesum} *} |
18 |
18 |
19 ML{*fun make_sum t1 t2 = |
19 ML{*fun make_sum t1 t2 = |
20 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
20 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
21 |
21 |
22 text {* \solution{ex:scancmts} *} |
22 text {* \solution{ex:scancmts} *} |
23 |
23 |
24 ML{*val any = Scan.one (Symbol.not_eof); |
24 ML{*val any = Scan.one (Symbol.not_eof) |
25 |
25 |
26 val scan_cmt = |
26 val scan_cmt = |
27 let |
27 let |
28 val begin_cmt = Scan.this_string "(*" |
28 val begin_cmt = Scan.this_string "(*" |
29 val end_cmt = Scan.this_string "*)" |
29 val end_cmt = Scan.this_string "*)" |
30 in |
30 in |
31 begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt |
31 begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt |
32 >> (enclose "(**" "**)" o implode) |
32 >> (enclose "(**" "**)" o implode) |
33 end |
33 end |
34 |
34 |
|
35 val parser = Scan.repeat (scan_cmt || any) |
|
36 |
35 val scan_all = |
37 val scan_all = |
36 Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) |
38 Scan.finite Symbol.stopper parser >> implode #> fst *} |
37 >> implode #> fst *} |
|
38 |
39 |
39 text {* |
40 text {* |
40 By using @{text "#> fst"} in the last line, the function |
41 By using @{text "#> fst"} in the last line, the function |
41 @{ML scan_all} retruns a string, instead of the pair a parser would |
42 @{ML scan_all} retruns a string, instead of the pair a parser would |
42 normally return. For example: |
43 normally return. For example: |
43 |
44 |
44 @{ML_response [display,gray] |
45 @{ML_response [display,gray] |
45 "let |
46 "let |
46 val input1 = (explode \"foo bar\") |
47 val input1 = (explode \"foo bar\") |
47 val input2 = (explode \"foo (*test*) bar (*test*)\") |
48 val input2 = (explode \"foo (*test*) bar (*test*)\") |
48 in |
49 in |
49 (scan_all input1, scan_all input2) |
50 (scan_all input1, scan_all input2) |
50 end" |
51 end" |
51 "(\"foo bar\",\"foo (**test**) bar (**test**)\")"} |
52 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"} |
52 *} |
53 *} |
53 |
54 |
|
55 text {* \solution{ex:addsimproc} *} |
|
56 |
|
57 ML{*fun dest_sum term = |
|
58 case term of |
|
59 (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) => |
|
60 (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2)) |
|
61 | _ => raise TERM ("dest_sum", [term]) |
|
62 |
|
63 fun get_sum_thm ctxt t (n1, n2) = |
|
64 let |
|
65 val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2) |
|
66 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, sum)) |
|
67 in |
|
68 mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1))) |
54 end |
69 end |
|
70 |
|
71 fun add_sp_aux ss t = |
|
72 let |
|
73 val ctxt = Simplifier.the_context ss |
|
74 val t' = term_of t |
|
75 in |
|
76 SOME (get_sum_thm ctxt t' (dest_sum t')) |
|
77 handle TERM _ => NONE |
|
78 end*} |
|
79 |
|
80 text {* The setup for the simproc is *} |
|
81 |
|
82 simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *} |
|
83 |
|
84 text {* and a test case is the lemma *} |
|
85 |
|
86 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
|
87 apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc add_sp}]) 1 *}) |
|
88 txt {* |
|
89 where the simproc produces the goal state |
|
90 |
|
91 \begin{minipage}{\textwidth} |
|
92 @{subgoals [display]} |
|
93 \end{minipage} |
|
94 *}(*<*)oops(*>*) |
|
95 |
|
96 |
|
97 |
|
98 end |