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] = Ord.order_antisym; (* <= <= = *) |
10 theorems [trans] = Ord.order_trans; (* <= <= <= *) |
11 theorems [trans] = Ord.order_trans; (* <= <= <= *) |
11 theorems [trans] = Ord.order_less_trans; (* < < < *) |
12 theorems [trans] = Ord.order_less_trans; (* < < < *) |
12 theorems [trans] = Ord.order_le_less_trans; (* <= < < *) |
13 theorems [trans] = Ord.order_le_less_trans; (* <= < < *) |
13 theorems [trans] = Ord.order_less_le_trans; (* < <= < *) |
14 theorems [trans] = Ord.order_less_le_trans; (* < <= < *) |
14 theorems [trans] = Ord.order_antisym; (* <= <= = *) |
|
15 |
15 |
16 theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; |
16 theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) |
17 by (rule HOL.subst[with y z]); |
17 by (rule HOL.subst[with y z]); |
18 |
18 |
19 theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; |
19 theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) |
20 by (rule HOL.ssubst[with x y]); |
20 by (rule HOL.ssubst[with x y]); |
21 |
21 |
22 theorem [trans]: "[| x < y; y = z |] ==> x < z"; |
22 theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) |
23 by (rule HOL.subst[with y z]); |
23 by (rule HOL.subst[with y z]); |
24 |
24 |
25 theorem [trans]: "[| x = y; y < z |] ==> x < z"; |
25 theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
26 by (rule HOL.ssubst[with x y]); |
26 by (rule HOL.ssubst[with x y]); |
27 |
27 |
28 theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *) |
28 theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *) |
29 theorems [trans] = HOL.ssubst; (* = x x *) |
29 theorems [trans] = HOL.ssubst; (* = x x *) |
30 |
30 |