82 simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *} |
82 simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *} |
83 |
83 |
84 text {* and a test case is the lemma *} |
84 text {* and a test case is the lemma *} |
85 |
85 |
86 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
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 *}) |
87 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *}) |
88 txt {* |
88 txt {* |
89 where the simproc produces the goal state |
89 where the simproc produces the goal state |
90 |
90 |
91 \begin{minipage}{\textwidth} |
91 \begin{minipage}{\textwidth} |
92 @{subgoals [display]} |
92 @{subgoals [display]} |
130 \begin{minipage}{\textwidth} |
130 \begin{minipage}{\textwidth} |
131 @{subgoals [display]} |
131 @{subgoals [display]} |
132 \end{minipage}\bigskip |
132 \end{minipage}\bigskip |
133 *}(*<*)oops(*>*) |
133 *}(*<*)oops(*>*) |
134 |
134 |
|
135 subsection {* Tests start here *} |
|
136 |
|
137 lemma cheat: "P" sorry |
|
138 |
|
139 ML{*fun timing_wrapper tac st = |
|
140 let |
|
141 val t_start = start_timing (); |
|
142 val res = tac st; |
|
143 val t_end = end_timing t_start; |
|
144 in |
|
145 (warning (#message t_end); res) |
|
146 end*} |
|
147 |
|
148 ML{* |
|
149 fun create_term1 0 = @{term "0::nat"} |
|
150 | create_term1 n = |
|
151 Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) |
|
152 $ (HOLogic.mk_number @{typ "nat"} n) $ (create_term1 (n-1)) |
|
153 *} |
|
154 |
|
155 ML{* |
|
156 fun create_term2 0 = @{term "0::nat"} |
|
157 | create_term2 n = |
|
158 Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) |
|
159 $ (create_term2 (n-1)) $ (HOLogic.mk_number @{typ nat} n) |
|
160 *} |
|
161 |
|
162 ML{* |
|
163 fun create_term n = |
|
164 HOLogic.mk_Trueprop |
|
165 (@{term "P::nat\<Rightarrow> bool"} $ |
|
166 (Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) |
|
167 $ (create_term1 n) $ (create_term2 n))) |
|
168 *} |
|
169 |
|
170 ML {* |
|
171 warning (Syntax.string_of_term @{context} (create_term 4)) |
|
172 *} |
|
173 |
|
174 ML {* |
|
175 val _ = Goal.prove @{context} [] [] (create_term 100) |
|
176 (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}])) |
|
177 *} |
|
178 |
|
179 ML {* |
|
180 val _ = Goal.prove @{context} [] [] (create_term 100) |
|
181 (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}])) |
|
182 *} |
|
183 |
|
184 ML {* |
|
185 val _ = Goal.prove @{context} [] [] (create_term 400) |
|
186 (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}])) |
|
187 *} |
|
188 |
|
189 ML {* |
|
190 val _ = Goal.prove @{context} [] [] (create_term 400) |
|
191 (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}])) |
|
192 *} |
135 |
193 |
136 end |
194 end |