1 (* Title: HOL/Calculation.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Setup transitivity rules for calculational proofs. |
|
7 *) |
|
8 |
|
9 theory Calculation = IntArith: |
|
10 |
|
11 lemma forw_subst: "a = b ==> P b ==> P a" |
|
12 by (rule ssubst) |
|
13 |
|
14 lemma back_subst: "P a ==> a = b ==> P b" |
|
15 by (rule subst) |
|
16 |
|
17 lemma set_rev_mp: "x:A ==> A <= B ==> x:B" |
|
18 by (rule subsetD) |
|
19 |
|
20 lemma set_mp: "A <= B ==> x:A ==> x:B" |
|
21 by (rule subsetD) |
|
22 |
|
23 lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b" |
|
24 by (simp add: order_less_le) |
|
25 |
|
26 lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b" |
|
27 by (simp add: order_less_le) |
|
28 |
|
29 lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P" |
|
30 by (rule order_less_asym) |
|
31 |
|
32 lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" |
|
33 by (rule subst) |
|
34 |
|
35 lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" |
|
36 by (rule ssubst) |
|
37 |
|
38 lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" |
|
39 by (rule subst) |
|
40 |
|
41 lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" |
|
42 by (rule ssubst) |
|
43 |
|
44 lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> |
|
45 (!!x y. x < y ==> f x < f y) ==> f a < c" |
|
46 proof - |
|
47 assume r: "!!x y. x < y ==> f x < f y" |
|
48 assume "a < b" hence "f a < f b" by (rule r) |
|
49 also assume "f b < c" |
|
50 finally (order_less_trans) show ?thesis . |
|
51 qed |
|
52 |
|
53 lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> |
|
54 (!!x y. x < y ==> f x < f y) ==> a < f c" |
|
55 proof - |
|
56 assume r: "!!x y. x < y ==> f x < f y" |
|
57 assume "a < f b" |
|
58 also assume "b < c" hence "f b < f c" by (rule r) |
|
59 finally (order_less_trans) show ?thesis . |
|
60 qed |
|
61 |
|
62 lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> |
|
63 (!!x y. x <= y ==> f x <= f y) ==> f a < c" |
|
64 proof - |
|
65 assume r: "!!x y. x <= y ==> f x <= f y" |
|
66 assume "a <= b" hence "f a <= f b" by (rule r) |
|
67 also assume "f b < c" |
|
68 finally (order_le_less_trans) show ?thesis . |
|
69 qed |
|
70 |
|
71 lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> |
|
72 (!!x y. x < y ==> f x < f y) ==> a < f c" |
|
73 proof - |
|
74 assume r: "!!x y. x < y ==> f x < f y" |
|
75 assume "a <= f b" |
|
76 also assume "b < c" hence "f b < f c" by (rule r) |
|
77 finally (order_le_less_trans) show ?thesis . |
|
78 qed |
|
79 |
|
80 lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> |
|
81 (!!x y. x < y ==> f x < f y) ==> f a < c" |
|
82 proof - |
|
83 assume r: "!!x y. x < y ==> f x < f y" |
|
84 assume "a < b" hence "f a < f b" by (rule r) |
|
85 also assume "f b <= c" |
|
86 finally (order_less_le_trans) show ?thesis . |
|
87 qed |
|
88 |
|
89 lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> |
|
90 (!!x y. x <= y ==> f x <= f y) ==> a < f c" |
|
91 proof - |
|
92 assume r: "!!x y. x <= y ==> f x <= f y" |
|
93 assume "a < f b" |
|
94 also assume "b <= c" hence "f b <= f c" by (rule r) |
|
95 finally (order_less_le_trans) show ?thesis . |
|
96 qed |
|
97 |
|
98 lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> |
|
99 (!!x y. x <= y ==> f x <= f y) ==> a <= f c" |
|
100 proof - |
|
101 assume r: "!!x y. x <= y ==> f x <= f y" |
|
102 assume "a <= f b" |
|
103 also assume "b <= c" hence "f b <= f c" by (rule r) |
|
104 finally (order_trans) show ?thesis . |
|
105 qed |
|
106 |
|
107 lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> |
|
108 (!!x y. x <= y ==> f x <= f y) ==> f a <= c" |
|
109 proof - |
|
110 assume r: "!!x y. x <= y ==> f x <= f y" |
|
111 assume "a <= b" hence "f a <= f b" by (rule r) |
|
112 also assume "f b <= c" |
|
113 finally (order_trans) show ?thesis . |
|
114 qed |
|
115 |
|
116 lemma ord_le_eq_subst: "a <= b ==> f b = c ==> |
|
117 (!!x y. x <= y ==> f x <= f y) ==> f a <= c" |
|
118 proof - |
|
119 assume r: "!!x y. x <= y ==> f x <= f y" |
|
120 assume "a <= b" hence "f a <= f b" by (rule r) |
|
121 also assume "f b = c" |
|
122 finally (ord_le_eq_trans) show ?thesis . |
|
123 qed |
|
124 |
|
125 lemma ord_eq_le_subst: "a = f b ==> b <= c ==> |
|
126 (!!x y. x <= y ==> f x <= f y) ==> a <= f c" |
|
127 proof - |
|
128 assume r: "!!x y. x <= y ==> f x <= f y" |
|
129 assume "a = f b" |
|
130 also assume "b <= c" hence "f b <= f c" by (rule r) |
|
131 finally (ord_eq_le_trans) show ?thesis . |
|
132 qed |
|
133 |
|
134 lemma ord_less_eq_subst: "a < b ==> f b = c ==> |
|
135 (!!x y. x < y ==> f x < f y) ==> f a < c" |
|
136 proof - |
|
137 assume r: "!!x y. x < y ==> f x < f y" |
|
138 assume "a < b" hence "f a < f b" by (rule r) |
|
139 also assume "f b = c" |
|
140 finally (ord_less_eq_trans) show ?thesis . |
|
141 qed |
|
142 |
|
143 lemma ord_eq_less_subst: "a = f b ==> b < c ==> |
|
144 (!!x y. x < y ==> f x < f y) ==> a < f c" |
|
145 proof - |
|
146 assume r: "!!x y. x < y ==> f x < f y" |
|
147 assume "a = f b" |
|
148 also assume "b < c" hence "f b < f c" by (rule r) |
|
149 finally (ord_eq_less_trans) show ?thesis . |
|
150 qed |
|
151 |
|
152 text {* |
|
153 Note that this list of rules is in reverse order of priorities. |
|
154 *} |
|
155 |
|
156 lemmas basic_trans_rules [trans] = |
|
157 order_less_subst2 |
|
158 order_less_subst1 |
|
159 order_le_less_subst2 |
|
160 order_le_less_subst1 |
|
161 order_less_le_subst2 |
|
162 order_less_le_subst1 |
|
163 order_subst2 |
|
164 order_subst1 |
|
165 ord_le_eq_subst |
|
166 ord_eq_le_subst |
|
167 ord_less_eq_subst |
|
168 ord_eq_less_subst |
|
169 forw_subst |
|
170 back_subst |
|
171 dvd_trans |
|
172 rev_mp |
|
173 mp |
|
174 set_rev_mp |
|
175 set_mp |
|
176 order_neq_le_trans |
|
177 order_le_neq_trans |
|
178 order_less_trans |
|
179 order_less_asym' |
|
180 order_le_less_trans |
|
181 order_less_le_trans |
|
182 order_trans |
|
183 order_antisym |
|
184 ord_le_eq_trans |
|
185 ord_eq_le_trans |
|
186 ord_less_eq_trans |
|
187 ord_eq_less_trans |
|
188 transitive |
|
189 trans |
|
190 |
|
191 end |
|