197 and "(x::int) + 1 > x" |
197 and "(x::int) + 1 > x" |
198 shows "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x" |
198 shows "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x" |
199 by (rewrite at "x + 1" in for (x) at asm add.commute) |
199 by (rewrite at "x + 1" in for (x) at asm add.commute) |
200 (rule assms) |
200 (rule assms) |
201 |
201 |
|
202 (* The rewrite method also has an ML interface *) |
|
203 lemma |
|
204 assumes "\<And>a b. P ((a + 1) * (1 + b)) " |
|
205 shows "\<And>a b :: nat. P ((a + 1) * (b + 1))" |
|
206 apply (tactic \<open> |
|
207 let |
|
208 val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} |
|
209 (* Note that the pattern order is reversed *) |
|
210 val pat = [ |
|
211 Rewrite.For [(x, SOME @{typ nat})], |
|
212 Rewrite.In, |
|
213 Rewrite.Term (@{const plus(nat)} $ Free (x, @{typ nat}) $ @{term "1 :: nat"}, [])] |
|
214 val to = NONE |
|
215 in Rewrite.rewrite_tac ctxt (pat, to) @{thms add.commute} 1 end |
|
216 \<close>) |
|
217 apply (fact assms) |
|
218 done |
|
219 |
|
220 lemma |
|
221 assumes "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. a + b))" |
|
222 shows "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))" |
|
223 apply (tactic \<open> |
|
224 let |
|
225 val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} |
|
226 val pat = [ |
|
227 Rewrite.Concl, |
|
228 Rewrite.In, |
|
229 Rewrite.Term (Free ("Q", (@{typ "int"} --> TVar (("'b",0), [])) --> @{typ bool}) |
|
230 $ Abs ("x", @{typ int}, Rewrite.mk_hole 1 (@{typ int} --> TVar (("'b",0), [])) $ Bound 0), [(x, @{typ int})]), |
|
231 Rewrite.In, |
|
232 Rewrite.Term (@{const plus(int)} $ Free (x, @{typ int}) $ Var (("c", 0), @{typ int}), []) |
|
233 ] |
|
234 val to = NONE |
|
235 in Rewrite.rewrite_tac ctxt (pat, to) @{thms add.commute} 1 end |
|
236 \<close>) |
|
237 apply (fact assms) |
|
238 done |
|
239 |
|
240 (* There is also conversion-like rewrite function: *) |
|
241 ML \<open> |
|
242 val ct = @{cprop "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))"} |
|
243 val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} |
|
244 val pat = [ |
|
245 Rewrite.Concl, |
|
246 Rewrite.In, |
|
247 Rewrite.Term (Free ("Q", (@{typ "int"} --> TVar (("'b",0), [])) --> @{typ bool}) |
|
248 $ Abs ("x", @{typ int}, Rewrite.mk_hole 1 (@{typ int} --> TVar (("'b",0), [])) $ Bound 0), [(x, @{typ int})]), |
|
249 Rewrite.In, |
|
250 Rewrite.Term (@{const plus(int)} $ Free (x, @{typ int}) $ Var (("c", 0), @{typ int}), []) |
|
251 ] |
|
252 val to = NONE |
|
253 val ct_ths = Rewrite.rewrite ctxt (pat, to) @{thms add.commute} ct |
|
254 |> Seq.list_of |
|
255 \<close> |
|
256 |
202 end |
257 end |
203 |
258 |