author | wenzelm |
Fri, 27 Aug 1999 20:29:20 +0200 | |
changeset 7381 | 1bd8633e8f90 |
parent 7202 | 6fcaf006cc40 |
child 7561 | ff8dbd0589aa |
permissions | -rw-r--r-- |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Calculation.thy |
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
4 |
|
6873 | 5 |
Setup transitivity rules for calculational proofs. Note that in the |
6 |
list below later rules have priority. |
|
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
7 |
*) |
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
8 |
|
6862 | 9 |
theory Calculation = Int:; |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
10 |
|
6945 | 11 |
|
7381 | 12 |
theorem [trans]: "[| s = t; P t |] ==> P s"; (* = x x *) |
13 |
by (rule ssubst); |
|
6873 | 14 |
|
7381 | 15 |
theorem [trans]: "[| P s; s = t |] ==> P t"; (* x = x *) |
16 |
by (rule subst); |
|
17 |
||
18 |
theorems [trans] = dvd_trans; (* dvd dvd dvd *) |
|
7202 | 19 |
|
20 |
theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"; (* < > P *) |
|
7381 | 21 |
by (rule order_less_asym); |
6873 | 22 |
|
7381 | 23 |
theorems [trans] = order_less_trans; (* < < < *) |
24 |
theorems [trans] = order_le_less_trans; (* <= < < *) |
|
25 |
theorems [trans] = order_less_le_trans; (* < <= < *) |
|
26 |
theorems [trans] = order_trans; (* <= <= <= *) |
|
27 |
theorems [trans] = order_antisym; (* <= >= = *) |
|
6862 | 28 |
|
7202 | 29 |
theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) |
7381 | 30 |
by (rule subst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
31 |
|
7202 | 32 |
theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) |
7381 | 33 |
by (rule ssubst); |
6862 | 34 |
|
7202 | 35 |
theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) |
7381 | 36 |
by (rule subst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
37 |
|
7202 | 38 |
theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
7381 | 39 |
by (rule ssubst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
40 |
|
7381 | 41 |
theorems [trans] = trans (* = = = *) |
6945 | 42 |
|
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
43 |
|
6862 | 44 |
end; |