1 (* Title: HOL/Calculation.thy |
1 (* Title: HOL/Calculation.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Setup transitivity rules for calculational proofs. |
5 Setup transitivity rules for calculational proofs. Note that in the |
|
6 list below later rules have priority. |
6 *) |
7 *) |
7 |
8 |
8 theory Calculation = Int:; |
9 theory Calculation = Int:; |
9 |
10 |
10 theorems [trans] = Ord.order_antisym; (* <= <= = *) |
11 theorems [trans] = HOL.ssubst; (* = x x *) |
11 theorems [trans] = Ord.order_trans; (* <= <= <= *) |
12 theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *) |
|
13 |
|
14 theorems [trans] = Divides.dvd_trans; (* dvd dvd dvd *) |
|
15 |
12 theorems [trans] = Ord.order_less_trans; (* < < < *) |
16 theorems [trans] = Ord.order_less_trans; (* < < < *) |
13 theorems [trans] = Ord.order_le_less_trans; (* <= < < *) |
17 theorems [trans] = Ord.order_le_less_trans; (* <= < < *) |
14 theorems [trans] = Ord.order_less_le_trans; (* < <= < *) |
18 theorems [trans] = Ord.order_less_le_trans; (* < <= < *) |
|
19 theorems [trans] = Ord.order_trans; (* <= <= <= *) |
|
20 theorems [trans] = Ord.order_antisym; (* <= <= = *) |
15 |
21 |
16 theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) |
22 theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) |
17 by (rule HOL.subst[with y z]); |
23 by (rule HOL.subst); |
18 |
24 |
19 theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) |
25 theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) |
20 by (rule HOL.ssubst[with x y]); |
26 by (rule HOL.ssubst); |
21 |
27 |
22 theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) |
28 theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) |
23 by (rule HOL.subst[with y z]); |
29 by (rule HOL.subst); |
24 |
30 |
25 theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
31 theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
26 by (rule HOL.ssubst[with x y]); |
32 by (rule HOL.ssubst); |
27 |
|
28 theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *) |
|
29 theorems [trans] = HOL.ssubst; (* = x x *) |
|
30 |
|
31 theorems [trans] = Divides.dvd_trans; (* dvd dvd dvd *) |
|
32 |
33 |
33 |
34 |
34 end; |
35 end; |