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. |
6 *) |
6 *) |
7 |
7 |
8 theory Calculation = Int: |
8 theory Calculation = Int:; |
9 |
9 |
10 theorems[trans] = HOL.ssubst (* = x x *) |
10 theorems [trans] = Ord.order_trans; (* <= <= <= *) |
11 theorems[trans] = HOL.subst[COMP swap_prems_rl] (* x = x *) |
11 theorems [trans] = Ord.order_less_trans; (* < < < *) |
|
12 theorems [trans] = Ord.order_le_less_trans; (* <= < < *) |
|
13 theorems [trans] = Ord.order_less_le_trans; (* < <= < *) |
|
14 theorems [trans] = Ord.order_antisym; (* <= <= = *) |
12 |
15 |
13 theorems[trans] = Ord.order_trans (* <= <= <= *) |
16 theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; |
14 theorems[trans] = Ord.order_less_trans (* < < < *) |
17 by (rule HOL.subst[with y z]); |
15 theorems[trans] = Ord.order_le_less_trans (* <= < < *) |
|
16 theorems[trans] = Ord.order_less_le_trans (* < <= < *) |
|
17 theorems[trans] = Ord.order_antisym (* <= <= = *) |
|
18 |
18 |
19 theorems[trans] = Divides.dvd_trans (* dvd dvd dvd *) |
19 theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; |
|
20 by (rule HOL.ssubst[with x y]); |
|
21 |
|
22 theorem [trans]: "[| x < y; y = z |] ==> x < z"; |
|
23 by (rule HOL.subst[with y z]); |
|
24 |
|
25 theorem [trans]: "[| x = y; y < z |] ==> x < z"; |
|
26 by (rule HOL.ssubst[with x y]); |
|
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 *) |
20 |
32 |
21 |
33 |
22 end |
34 end; |