20 (* Selecting a specific subterm in a large, ambiguous term. *) |
20 (* Selecting a specific subterm in a large, ambiguous term. *) |
21 lemma |
21 lemma |
22 fixes a b c :: int |
22 fixes a b c :: int |
23 assumes "f (a - a + (a - a)) + f ( 0 + c) = f 0 + f c" |
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" |
24 shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
25 by (rewrite in "f _ + f \<box> = _" diff_self) fact |
25 by (rewrite in "f _ + f \<hole> = _" diff_self) fact |
26 |
26 |
27 lemma |
27 lemma |
28 fixes a b c :: int |
28 fixes a b c :: int |
29 assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" |
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" |
30 shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
31 by (rewrite at "f (_ + \<box>) + f _ = _" diff_self) fact |
31 by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact |
32 |
32 |
33 lemma |
33 lemma |
34 fixes a b c :: int |
34 fixes a b c :: int |
35 assumes "f ( 0 + (a - a)) + f ((a - a) + c) = f 0 + f c" |
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" |
36 shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
37 by (rewrite in "f (\<box> + _) + _ = _" diff_self) fact |
37 by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact |
38 |
38 |
39 lemma |
39 lemma |
40 fixes a b c :: int |
40 fixes a b c :: int |
41 assumes "f (a - a + 0 ) + f ((a - a) + c) = f 0 + f c" |
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" |
42 shows "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c" |
43 by (rewrite in "f (_ + \<box>) + _ = _" diff_self) fact |
43 by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact |
44 |
44 |
45 lemma |
45 lemma |
46 fixes x y :: nat |
46 fixes x y :: nat |
47 shows"x + y > c \<Longrightarrow> y + x > c" |
47 shows"x + y > c \<Longrightarrow> y + x > c" |
48 by (rewrite at "\<box> > c" add.commute) assumption |
48 by (rewrite at "\<hole> > c" add.commute) assumption |
49 |
49 |
50 (* We can also rewrite in the assumptions. *) |
50 (* We can also rewrite in the assumptions. *) |
51 lemma |
51 lemma |
52 fixes x y :: nat |
52 fixes x y :: nat |
53 assumes "y + x > c \<Longrightarrow> y + x > c" |
53 assumes "y + x > c \<Longrightarrow> y + x > c" |
62 |
62 |
63 lemma |
63 lemma |
64 fixes x y :: nat |
64 fixes x y :: nat |
65 assumes "y + x > c \<Longrightarrow> y + x > c" |
65 assumes "y + x > c \<Longrightarrow> y + x > c" |
66 shows "x + y > c \<Longrightarrow> y + x > c" |
66 shows "x + y > c \<Longrightarrow> y + x > c" |
67 by (rewrite at "\<box> > c" at asm add.commute) fact |
67 by (rewrite at "\<hole> > c" at asm add.commute) fact |
68 |
68 |
69 lemma |
69 lemma |
70 assumes "P {x::int. y + 1 = 1 + x}" |
70 assumes "P {x::int. y + 1 = 1 + x}" |
71 shows "P {x::int. y + 1 = x + 1}" |
71 shows "P {x::int. y + 1 = x + 1}" |
72 by (rewrite at "x+1" in "{x::int. \<box> }" add.commute) fact |
72 by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact |
73 |
73 |
74 lemma |
74 lemma |
75 assumes "P {x::int. y + 1 = 1 + x}" |
75 assumes "P {x::int. y + 1 = 1 + x}" |
76 shows "P {x::int. y + 1 = x + 1}" |
76 shows "P {x::int. y + 1 = x + 1}" |
77 by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<box> }" add.commute) |
77 by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute) |
78 fact |
78 fact |
79 |
79 |
80 lemma |
80 lemma |
81 assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}" |
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)}" |
82 shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}" |
83 by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<box>)" add.commute) fact |
83 by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact |
84 |
84 |
85 |
85 |
86 (* Rewriting with conditional rewriting rules works just as well. *) |
86 (* Rewriting with conditional rewriting rules works just as well. *) |
87 lemma test_theorem: |
87 lemma test_theorem: |
88 fixes x :: nat |
88 fixes x :: nat |
124 (* We can also add an invariant that contains the variable n bound in the outer context. |
124 (* We can also add an invariant that contains the variable n bound in the outer context. |
125 For this, we need to bind this variable to an identifier. *) |
125 For this, we need to bind this variable to an identifier. *) |
126 lemma |
126 lemma |
127 assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
127 assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
128 shows "P (\<lambda>n. f n + 1) = x" |
128 shows "P (\<lambda>n. f n + 1) = x" |
129 by (rewrite in "\<lambda>n. \<box>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact |
129 by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact |
130 |
130 |
131 (* Any identifier will work *) |
131 (* Any identifier will work *) |
132 lemma |
132 lemma |
133 assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
133 assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x" |
134 shows "P (\<lambda>n. f n + 1) = x" |
134 shows "P (\<lambda>n. f n + 1) = x" |
135 by (rewrite in "\<lambda>abc. \<box>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact |
135 by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact |
136 |
136 |
137 (* The "for" keyword. *) |
137 (* The "for" keyword. *) |
138 lemma |
138 lemma |
139 assumes "P (2 + 1)" |
139 assumes "P (2 + 1)" |
140 shows "\<And>x y. P (1 + 2 :: nat)" |
140 shows "\<And>x y. P (1 + 2 :: nat)" |
156 by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact |
156 by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact |
157 |
157 |
158 lemma |
158 lemma |
159 assumes "\<And>x y z. x + y + z = y + z + (x::int)" |
159 assumes "\<And>x y z. x + y + z = y + z + (x::int)" |
160 shows "\<And>x y z. x + y + z = z + y + (x::int)" |
160 shows "\<And>x y z. x + y + z = z + y + (x::int)" |
161 by (rewrite at "\<box> + _" at "_ = \<box>" in concl at for () add.commute) fact |
161 by (rewrite at "\<hole> + _" at "_ = \<hole>" in concl at for () add.commute) fact |
162 |
162 |
163 (* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *) |
163 (* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *) |
164 lemma |
164 lemma |
165 assumes "(\<And>(x::int). x < 1 + x)" |
165 assumes "(\<And>(x::int). x < 1 + x)" |
166 and "(x::int) + 1 > x" |
166 and "(x::int) + 1 > x" |