author | wenzelm |
Fri, 23 Nov 2018 16:43:11 +0100 | |
changeset 69334 | 6b49700da068 |
parent 66453 | cc19f7ca2ed6 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
59739 | 1 |
theory Rewrite_Examples |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
60117
diff
changeset
|
2 |
imports Main "HOL-Library.Rewrite" |
59739 | 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 |
lemma |
|
13 |
fixes a::int and b::int and c::int |
|
14 |
assumes "P (b + a)" |
|
15 |
shows "P (a + b)" |
|
16 |
by (rewrite at "a + b" add.commute) |
|
17 |
(rule assms) |
|
18 |
||
19 |
(* Selecting a specific subterm in a large, ambiguous term. *) |
|
20 |
lemma |
|
21 |
fixes a b c :: int |
|
22 |
assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c" |
|
23 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 24 |
by (rewrite in "f _ + f \<hole> = _" diff_self) fact |
59739 | 25 |
|
26 |
lemma |
|
27 |
fixes a b c :: int |
|
28 |
assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" |
|
29 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 30 |
by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact |
59739 | 31 |
|
32 |
lemma |
|
33 |
fixes a b c :: int |
|
34 |
assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
35 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 36 |
by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact |
59739 | 37 |
|
38 |
lemma |
|
39 |
fixes a b c :: int |
|
40 |
assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" |
|
41 |
shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
|
60047 | 42 |
by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact |
59739 | 43 |
|
44 |
lemma |
|
45 |
fixes x y :: nat |
|
46 |
shows"x + y > c \<Longrightarrow> y + x > c" |
|
60047 | 47 |
by (rewrite at "\<hole> > c" add.commute) assumption |
59739 | 48 |
|
49 |
(* We can also rewrite in the assumptions. *) |
|
50 |
lemma |
|
51 |
fixes x y :: nat |
|
52 |
assumes "y + x > c \<Longrightarrow> y + x > c" |
|
53 |
shows "x + y > c \<Longrightarrow> y + x > c" |
|
54 |
by (rewrite in asm add.commute) fact |
|
55 |
||
56 |
lemma |
|
57 |
fixes x y :: nat |
|
58 |
assumes "y + x > c \<Longrightarrow> y + x > c" |
|
59 |
shows "x + y > c \<Longrightarrow> y + x > c" |
|
60 |
by (rewrite in "x + y > c" at asm add.commute) fact |
|
61 |
||
62 |
lemma |
|
63 |
fixes x y :: nat |
|
64 |
assumes "y + x > c \<Longrightarrow> y + x > c" |
|
65 |
shows "x + y > c \<Longrightarrow> y + x > c" |
|
60047 | 66 |
by (rewrite at "\<hole> > c" at asm add.commute) fact |
59739 | 67 |
|
68 |
lemma |
|
69 |
assumes "P {x::int. y + 1 = 1 + x}" |
|
70 |
shows "P {x::int. y + 1 = x + 1}" |
|
60047 | 71 |
by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact |
59739 | 72 |
|
73 |
lemma |
|
74 |
assumes "P {x::int. y + 1 = 1 + x}" |
|
75 |
shows "P {x::int. y + 1 = x + 1}" |
|
60047 | 76 |
by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute) |
59739 | 77 |
fact |
78 |
||
79 |
lemma |
|
80 |
assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}" |
|
81 |
shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}" |
|
60047 | 82 |
by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact |
59739 | 83 |
|
60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
84 |
(* 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
|
85 |
lemma |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
by (rewrite at asm assms) |
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
89 |
|
60117 | 90 |
lemma |
91 |
assumes "PROP P \<equiv> PROP Q" |
|
92 |
shows "PROP R \<Longrightarrow> PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q" |
|
93 |
by (rewrite at asm assms) |
|
94 |
||
60053
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
95 |
(* 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
|
96 |
lemma |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
97 |
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
|
98 |
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
|
99 |
apply (rewrite at asm assms) |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
100 |
apply assumption |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
101 |
done |
0e9895ffab1d
rewrite: do not descend into conclusion of premise with asm pattern
noschinl
parents:
60052
diff
changeset
|
102 |
|
60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60050
diff
changeset
|
103 |
|
59739 | 104 |
|
105 |
(* Rewriting with conditional rewriting rules works just as well. *) |
|
106 |
lemma test_theorem: |
|
107 |
fixes x :: nat |
|
108 |
shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y" |
|
109 |
by (rule Orderings.order_antisym) |
|
110 |
||
60050 | 111 |
(* Premises of the conditional rule yield new subgoals. The |
112 |
assumptions of the goal are propagated into these subgoals |
|
113 |
*) |
|
59739 | 114 |
lemma |
60050 | 115 |
fixes f :: "nat \<Rightarrow> nat" |
116 |
shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0" |
|
59739 | 117 |
apply (rewrite at "f x" to "0" test_theorem) |
60050 | 118 |
apply assumption |
119 |
apply assumption |
|
59739 | 120 |
apply (rule refl) |
60050 | 121 |
done |
59739 | 122 |
|
60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
123 |
(* 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
|
124 |
lemma |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
125 |
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
|
126 |
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
|
127 |
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
|
128 |
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
|
129 |
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
|
130 |
apply (rewrite at asm rewr) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
131 |
apply (fact A1) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
132 |
apply (fact A2) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
133 |
apply (fact C) |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
134 |
done |
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
135 |
|
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset
|
136 |
|
59739 | 137 |
(* |
138 |
Instantiation. |
|
139 |
||
140 |
Since all rewriting is now done via conversions, |
|
141 |
instantiation becomes fairly easy to do. |
|
142 |
*) |
|
143 |
||
144 |
(* We first introduce a function f and an extended |
|
145 |
version of f that is annotated with an invariant. *) |
|
146 |
fun f :: "nat \<Rightarrow> nat" where "f n = n" |
|
147 |
definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n" |
|
148 |
||
149 |
lemma annotate_f: "f = f_inv I" |
|
150 |
by (simp add: f_inv_def fun_eq_iff) |
|
151 |
||
152 |
(* We have a lemma with a bound variable n, and |
|
153 |
want to add an invariant to f. *) |
|
154 |
lemma |
|
155 |
assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x" |
|
156 |
shows "P (\<lambda>n. f n + 1) = x" |
|
157 |
by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact |
|
158 |
||
159 |
(* We can also add an invariant that contains the variable n bound in the outer context. |
|
160 |
For this, we need to bind this variable to an identifier. *) |
|
161 |
lemma |
|
162 |
assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
|
163 |
shows "P (\<lambda>n. f n + 1) = x" |
|
60047 | 164 |
by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact |
59739 | 165 |
|
166 |
(* Any identifier will work *) |
|
167 |
lemma |
|
168 |
assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
|
169 |
shows "P (\<lambda>n. f n + 1) = x" |
|
60047 | 170 |
by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact |
59739 | 171 |
|
172 |
(* The "for" keyword. *) |
|
173 |
lemma |
|
174 |
assumes "P (2 + 1)" |
|
175 |
shows "\<And>x y. P (1 + 2 :: nat)" |
|
176 |
by (rewrite in "P (1 + 2)" at for (x) add.commute) fact |
|
177 |
||
178 |
lemma |
|
179 |
assumes "\<And>x y. P (y + x)" |
|
180 |
shows "\<And>x y. P (x + y :: nat)" |
|
181 |
by (rewrite in "P (x + _)" at for (x y) add.commute) fact |
|
182 |
||
183 |
lemma |
|
184 |
assumes "\<And>x y z. y + x + z = z + y + (x::int)" |
|
185 |
shows "\<And>x y z. x + y + z = z + y + (x::int)" |
|
60108
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
186 |
by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact |
59739 | 187 |
|
188 |
lemma |
|
189 |
assumes "\<And>x y z. z + (x + y) = z + y + (x::int)" |
|
190 |
shows "\<And>x y z. x + y + z = z + y + (x::int)" |
|
60108
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
191 |
by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact |
59739 | 192 |
|
193 |
lemma |
|
194 |
assumes "\<And>x y z. x + y + z = y + z + (x::int)" |
|
195 |
shows "\<And>x y z. x + y + z = z + y + (x::int)" |
|
60108
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
196 |
by (rewrite at "\<hole> + _" at "_ = \<hole>" in for () add.commute) fact |
59739 | 197 |
|
60108
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
198 |
lemma |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
199 |
assumes eq: "\<And>x. P x \<Longrightarrow> g x = x" |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
200 |
assumes f1: "\<And>x. Q x \<Longrightarrow> P x" |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
201 |
assumes f2: "\<And>x. Q x \<Longrightarrow> x" |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
202 |
shows "\<And>x. Q x \<Longrightarrow> g x" |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
203 |
apply (rewrite at "g x" in for (x) eq) |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
204 |
apply (fact f1) |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
205 |
apply (fact f2) |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
206 |
done |
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
207 |
|
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset
|
208 |
(* The for keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *) |
59739 | 209 |
lemma |
210 |
assumes "(\<And>(x::int). x < 1 + x)" |
|
211 |
and "(x::int) + 1 > x" |
|
212 |
shows "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x" |
|
213 |
by (rewrite at "x + 1" in for (x) at asm add.commute) |
|
214 |
(rule assms) |
|
215 |
||
60079 | 216 |
(* The rewrite method also has an ML interface *) |
217 |
lemma |
|
218 |
assumes "\<And>a b. P ((a + 1) * (1 + b)) " |
|
219 |
shows "\<And>a b :: nat. P ((a + 1) * (b + 1))" |
|
220 |
apply (tactic \<open> |
|
221 |
let |
|
222 |
val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} |
|
223 |
(* Note that the pattern order is reversed *) |
|
224 |
val pat = [ |
|
225 |
Rewrite.For [(x, SOME @{typ nat})], |
|
226 |
Rewrite.In, |
|
227 |
Rewrite.Term (@{const plus(nat)} $ Free (x, @{typ nat}) $ @{term "1 :: nat"}, [])] |
|
228 |
val to = NONE |
|
60117 | 229 |
in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end |
60079 | 230 |
\<close>) |
231 |
apply (fact assms) |
|
232 |
done |
|
233 |
||
234 |
lemma |
|
235 |
assumes "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. a + b))" |
|
236 |
shows "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))" |
|
237 |
apply (tactic \<open> |
|
238 |
let |
|
239 |
val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} |
|
240 |
val pat = [ |
|
241 |
Rewrite.Concl, |
|
242 |
Rewrite.In, |
|
243 |
Rewrite.Term (Free ("Q", (@{typ "int"} --> TVar (("'b",0), [])) --> @{typ bool}) |
|
244 |
$ Abs ("x", @{typ int}, Rewrite.mk_hole 1 (@{typ int} --> TVar (("'b",0), [])) $ Bound 0), [(x, @{typ int})]), |
|
245 |
Rewrite.In, |
|
246 |
Rewrite.Term (@{const plus(int)} $ Free (x, @{typ int}) $ Var (("c", 0), @{typ int}), []) |
|
247 |
] |
|
248 |
val to = NONE |
|
60117 | 249 |
in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end |
60079 | 250 |
\<close>) |
251 |
apply (fact assms) |
|
252 |
done |
|
253 |
||
254 |
(* There is also conversion-like rewrite function: *) |
|
255 |
ML \<open> |
|
256 |
val ct = @{cprop "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))"} |
|
257 |
val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} |
|
258 |
val pat = [ |
|
259 |
Rewrite.Concl, |
|
260 |
Rewrite.In, |
|
261 |
Rewrite.Term (Free ("Q", (@{typ "int"} --> TVar (("'b",0), [])) --> @{typ bool}) |
|
262 |
$ Abs ("x", @{typ int}, Rewrite.mk_hole 1 (@{typ int} --> TVar (("'b",0), [])) $ Bound 0), [(x, @{typ int})]), |
|
263 |
Rewrite.In, |
|
264 |
Rewrite.Term (@{const plus(int)} $ Free (x, @{typ int}) $ Var (("c", 0), @{typ int}), []) |
|
265 |
] |
|
266 |
val to = NONE |
|
60117 | 267 |
val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct |
60079 | 268 |
\<close> |
269 |
||
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
270 |
section \<open>Regression tests\<close> |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
271 |
|
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
272 |
ML \<open> |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
273 |
val ct = @{cterm "(\<lambda>b :: int. (\<lambda>a. b + a))"} |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
274 |
val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context} |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
275 |
val pat = [ |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
276 |
Rewrite.In, |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
277 |
Rewrite.Term (@{const plus(int)} $ Var (("c", 0), @{typ int}) $ Var (("c", 0), @{typ int}), []) |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
278 |
] |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
279 |
val to = NONE |
60117 | 280 |
val _ = |
281 |
case try (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) ct of |
|
282 |
NONE => () |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
283 |
| _ => error "should not have matched anything" |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
284 |
\<close> |
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
285 |
|
60117 | 286 |
ML \<open> |
287 |
Rewrite.params_pconv (Conv.all_conv |> K |> K) @{context} (Vartab.empty, []) @{cterm "\<And>x. PROP A"} |
|
288 |
\<close> |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
289 |
|
60117 | 290 |
lemma |
291 |
assumes eq: "PROP A \<Longrightarrow> PROP B \<equiv> PROP C" |
|
292 |
assumes f1: "PROP D \<Longrightarrow> PROP A" |
|
293 |
assumes f2: "PROP D \<Longrightarrow> PROP C" |
|
294 |
shows "\<And>x. PROP D \<Longrightarrow> PROP B" |
|
295 |
apply (rewrite eq) |
|
296 |
apply (fact f1) |
|
297 |
apply (fact f2) |
|
298 |
done |
|
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset
|
299 |
|
59739 | 300 |
end |