equal
deleted
inserted
replaced
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 |
10 theorems[trans] = HOL.ssubst (* = x x *) |
11 theorems[trans] = HOL.trans (* = = = *) |
11 theorems[trans] = HOL.subst[COMP swap_prems_rl] (* x = x *) |
12 theorems[trans] = HOL.ssubst (* = * * *) |
|
13 theorems[trans] = HOL.subst[COMP swap_prems_rl] (* * = * *) |
|
14 |
12 |
15 theorems[trans] = Ord.order_trans (* <= <= <= *) |
13 theorems[trans] = Ord.order_trans (* <= <= <= *) |
16 theorems[trans] = Ord.order_less_trans (* < < < *) |
14 theorems[trans] = Ord.order_less_trans (* < < < *) |
17 theorems[trans] = Ord.order_le_less_trans (* <= < < *) |
15 theorems[trans] = Ord.order_le_less_trans (* <= < < *) |
18 theorems[trans] = Ord.order_less_le_trans (* < <= < *) |
16 theorems[trans] = Ord.order_less_le_trans (* < <= < *) |
|
17 theorems[trans] = Ord.order_antisym (* <= <= = *) |
19 |
18 |
20 theorems[trans] = Divides.dvd_trans (* dvd dvd dvd *) |
19 theorems[trans] = Divides.dvd_trans (* dvd dvd dvd *) |
21 |
20 |
22 |
21 |
23 end |
22 end |