author | wenzelm |
Thu, 14 Oct 1999 15:04:36 +0200 | |
changeset 7866 | 3ccaa11b6df9 |
parent 7657 | dbbf7721126e |
child 8229 | 38f453607c61 |
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 |
|
7657 | 20 |
theorem [trans]: "[| c:A; A <= B |] ==> c:B"; |
21 |
by (rule subsetD); |
|
22 |
||
23 |
theorem [trans]: "[| A <= B; c:A |] ==> c:B"; |
|
24 |
by (rule subsetD); |
|
25 |
||
7561 | 26 |
theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y"; (* ~= <= < *) |
27 |
by (simp! add: order_less_le); |
|
28 |
||
29 |
theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *) |
|
30 |
by (simp! add: order_less_le); |
|
31 |
||
7202 | 32 |
theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"; (* < > P *) |
7381 | 33 |
by (rule order_less_asym); |
6873 | 34 |
|
7381 | 35 |
theorems [trans] = order_less_trans; (* < < < *) |
36 |
theorems [trans] = order_le_less_trans; (* <= < < *) |
|
37 |
theorems [trans] = order_less_le_trans; (* < <= < *) |
|
38 |
theorems [trans] = order_trans; (* <= <= <= *) |
|
39 |
theorems [trans] = order_antisym; (* <= >= = *) |
|
6862 | 40 |
|
7202 | 41 |
theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) |
7381 | 42 |
by (rule subst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
43 |
|
7202 | 44 |
theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) |
7381 | 45 |
by (rule ssubst); |
6862 | 46 |
|
7202 | 47 |
theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) |
7381 | 48 |
by (rule subst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
49 |
|
7202 | 50 |
theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
7381 | 51 |
by (rule ssubst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
52 |
|
7381 | 53 |
theorems [trans] = trans (* = = = *) |
6945 | 54 |
|
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
55 |
|
6862 | 56 |
end; |