author | noschinl |
Wed, 15 Apr 2015 15:10:01 +0200 | |
changeset 60079 | ef4fe30e9ef1 |
parent 60054 | ef4878146485 |
child 60088 | 0a064330a885 |
permissions | -rw-r--r-- |
59739 | 1 |
theory Rewrite_Examples |
2 |
imports Main "~~/src/HOL/Library/Rewrite" |
|
3 |
begin |
|
4 |
||
5 |
section \<open>The rewrite Proof Method by Example\<close> |
|
6 |
||
7 |
(* This file is intended to give an overview over |
|
8 |
the features of the pattern-based rewrite proof method. |
|
9 |
||
10 |
See also https://www21.in.tum.de/~noschinl/Pattern-2014/ |
|
11 |
*) |
|
12 |
||
13 |
lemma |
|
14 |
fixes a::int and b::int and c::int |
|
15 |
assumes "P (b + a)" |
|
16 |
shows "P (a + b)" |
|
17 |
by (rewrite at "a + b" add.commute) |
|
18 |
(rule assms) |
|
19 |
||
20 |
(* Selecting a specific subterm in a large, ambiguous term. *) |
|
21 |
lemma |
|
22 |
fixes a b c :: int |
|
23 |
assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c" |
|
24 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 25 |
by (rewrite in "f _ + f \<hole> = _" diff_self) fact |
59739 | 26 |
|
27 |
lemma |
|
28 |
fixes a b c :: int |
|
29 |
assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" |
|
30 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 31 |
by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact |
59739 | 32 |
|
33 |
lemma |
|
34 |
fixes a b c :: int |
|
35 |
assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
36 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 37 |
by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact |
59739 | 38 |
|
39 |
lemma |
|
40 |
fixes a b c :: int |
|
41 |
assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" |
|
42 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 43 |
by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact |
59739 | 44 |
|
45 |
lemma |
|
46 |
fixes x y :: nat |
|
47 |
shows"x + y > c \<Longrightarrow> y + x > c" |
|
60047 | 48 |
by (rewrite at "\<hole> > c" add.commute) assumption |
59739 | 49 |
|
50 |
(* We can also rewrite in the assumptions. *) |
|
51 |
lemma |
|
52 |
fixes x y :: nat |
|
53 |
assumes "y + x > c \<Longrightarrow> y + x > c" |
|
54 |
shows "x + y > c \<Longrightarrow> y + x > c" |
|
55 |
by (rewrite in asm add.commute) fact |
|
56 |
||
57 |
lemma |
|
58 |
fixes x y :: nat |
|
59 |
assumes "y + x > c \<Longrightarrow> y + x > c" |
|
60 |
shows "x + y > c \<Longrightarrow> y + x > c" |
|
61 |
by (rewrite in "x + y > c" at asm add.commute) fact |
|
62 |
||
63 |
lemma |
|
64 |
fixes x y :: nat |
|
65 |
assumes "y + x > c \<Longrightarrow> y + x > c" |
|
66 |
shows "x + y > c \<Longrightarrow> y + x > c" |
|
60047 | 67 |
by (rewrite at "\<hole> > c" at asm add.commute) fact |
59739 | 68 |
|
69 |
lemma |
|
70 |
assumes "P {x::int. y + 1 = 1 + x}" |
|
71 |
shows "P {x::int. y + 1 = x + 1}" |
|
60047 | 72 |
by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact |
59739 | 73 |
|
74 |
lemma |
|
75 |
assumes "P {x::int. y + 1 = 1 + x}" |
|
76 |
shows "P {x::int. y + 1 = x + 1}" |
|
60047 | 77 |
by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute) |
59739 | 78 |
fact |
79 |
||
80 |
lemma |
|
81 |
assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}" |
|
82 |
shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}" |
|
60047 | 83 |
by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact |
59739 | 84 |
|
60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
85 |
(* This is not limited to the first assumption *) |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
86 |
lemma |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
87 |
assumes "PROP P \<equiv> PROP Q" |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
88 |
shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q" |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
89 |
by (rewrite at asm assms) |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
90 |
|
60053
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
91 |
(* Rewriting "at asm" selects each full assumption, not any parts *) |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
92 |
lemma |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
93 |
assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)" |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
94 |
shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R" |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
95 |
apply (rewrite at asm assms) |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
96 |
apply assumption |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
97 |
done |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
98 |
|
60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
99 |
|
59739 | 100 |
|
101 |
(* Rewriting with conditional rewriting rules works just as well. *) |
|
102 |
lemma test_theorem: |
|
103 |
fixes x :: nat |
|
104 |
shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y" |
|
105 |
by (rule Orderings.order_antisym) |
|
106 |
||
60050 | 107 |
(* Premises of the conditional rule yield new subgoals. The |
108 |
assumptions of the goal are propagated into these subgoals |
|
109 |
*) |
|
59739 | 110 |
lemma |
60050 | 111 |
fixes f :: "nat \<Rightarrow> nat" |
112 |
shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0" |
|
59739 | 113 |
apply (rewrite at "f x" to "0" test_theorem) |
60050 | 114 |
apply assumption |
115 |
apply assumption |
|
59739 | 116 |
apply (rule refl) |
60050 | 117 |
done |
59739 | 118 |
|
60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
119 |
(* This holds also for rewriting in assumptions. The order of assumptions is preserved *) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
120 |
lemma |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
121 |
assumes rewr: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP R \<equiv> PROP R'" |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
122 |
assumes A1: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP P" |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
123 |
assumes A2: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP Q" |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
124 |
assumes C: "PROP S \<Longrightarrow> PROP R' \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V" |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
125 |
shows "PROP S \<Longrightarrow> PROP R \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V" |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
126 |
apply (rewrite at asm rewr) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
127 |
apply (fact A1) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
128 |
apply (fact A2) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
129 |
apply (fact C) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
130 |
done |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
131 |
|
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
132 |
|
59739 | 133 |
(* |
134 |
Instantiation. |
|
135 |
||
136 |
Since all rewriting is now done via conversions, |
|
137 |
instantiation becomes fairly easy to do. |
|
138 |
*) |
|
139 |
||
140 |
(* We first introduce a function f and an extended |
|
141 |
version of f that is annotated with an invariant. *) |
|
142 |
fun f :: "nat \<Rightarrow> nat" where "f n = n" |
|
143 |
definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n" |
|
144 |
||
145 |
lemma annotate_f: "f = f_inv I" |
|
146 |
by (simp add: f_inv_def fun_eq_iff) |
|
147 |
||
148 |
(* We have a lemma with a bound variable n, and |
|
149 |
want to add an invariant to f. *) |
|
150 |
lemma |
|
151 |
assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x" |
|
152 |
shows "P (\<lambda>n. f n + 1) = x" |
|
153 |
by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact |
|
154 |
||
155 |
(* We can also add an invariant that contains the variable n bound in the outer context. |
|
156 |
For this, we need to bind this variable to an identifier. *) |
|
157 |
lemma |
|
158 |
assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
|
159 |
shows "P (\<lambda>n. f n + 1) = x" |
|
60047 | 160 |
by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact |
59739 | 161 |
|
162 |
(* Any identifier will work *) |
|
163 |
lemma |
|
164 |
assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
|
165 |
shows "P (\<lambda>n. f n + 1) = x" |
|
60047 | 166 |
by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact |
59739 | 167 |
|
168 |
(* The "for" keyword. *) |
|
169 |
lemma |
|
170 |
assumes "P (2 + 1)" |
|
171 |
shows "\<And>x y. P (1 + 2 :: nat)" |
|
172 |
by (rewrite in "P (1 + 2)" at for (x) add.commute) fact |
|
173 |
||
174 |
lemma |
|
175 |
assumes "\<And>x y. P (y + x)" |
|
176 |
shows "\<And>x y. P (x + y :: nat)" |
|
177 |
by (rewrite in "P (x + _)" at for (x y) add.commute) fact |
|
178 |
||
179 |
lemma |
|
180 |
assumes "\<And>x y z. y + x + z = z + y + (x::int)" |
|
181 |
shows "\<And>x y z. x + y + z = z + y + (x::int)" |
|
182 |
by (rewrite at "x + y" in "x + y + z" in concl at for (x y z) add.commute) fact |
|
183 |
||
184 |
lemma |
|
185 |
assumes "\<And>x y z. z + (x + y) = z + y + (x::int)" |
|
186 |
shows "\<And>x y z. x + y + z = z + y + (x::int)" |
|
187 |
by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact |
|
188 |
||
189 |
lemma |
|
190 |
assumes "\<And>x y z. x + y + z = y + z + (x::int)" |
|
191 |
shows "\<And>x y z. x + y + z = z + y + (x::int)" |
|
60047 | 192 |
by (rewrite at "\<hole> + _" at "_ = \<hole>" in concl at for () add.commute) fact |
59739 | 193 |
|
194 |
(* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *) |
|
195 |
lemma |
|
196 |
assumes "(\<And>(x::int). x < 1 + x)" |
|
197 |
and "(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) |
|
200 |
(rule assms) |
|
201 |
||
60079 | 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 |
||
59739 | 257 |
end |
258 |