author | wenzelm |
Mon, 13 Mar 2000 13:21:39 +0100 | |
changeset 8434 | 5e4bba59bfaa |
parent 8301 | d9345bad5e5c |
child 8855 | ef4848bb0696 |
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 |
|
8301 | 11 |
theorems [trans] = rev_mp mp; |
6945 | 12 |
|
7381 | 13 |
theorem [trans]: "[| s = t; P t |] ==> P s"; (* = x x *) |
14 |
by (rule ssubst); |
|
6873 | 15 |
|
7381 | 16 |
theorem [trans]: "[| P s; s = t |] ==> P t"; (* x = x *) |
17 |
by (rule subst); |
|
18 |
||
19 |
theorems [trans] = dvd_trans; (* dvd dvd dvd *) |
|
7202 | 20 |
|
7657 | 21 |
theorem [trans]: "[| c:A; A <= B |] ==> c:B"; |
22 |
by (rule subsetD); |
|
23 |
||
24 |
theorem [trans]: "[| A <= B; c:A |] ==> c:B"; |
|
25 |
by (rule subsetD); |
|
26 |
||
7561 | 27 |
theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y"; (* ~= <= < *) |
28 |
by (simp! add: order_less_le); |
|
29 |
||
30 |
theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *) |
|
31 |
by (simp! add: order_less_le); |
|
32 |
||
7202 | 33 |
theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"; (* < > P *) |
7381 | 34 |
by (rule order_less_asym); |
6873 | 35 |
|
7381 | 36 |
theorems [trans] = order_less_trans; (* < < < *) |
37 |
theorems [trans] = order_le_less_trans; (* <= < < *) |
|
38 |
theorems [trans] = order_less_le_trans; (* < <= < *) |
|
39 |
theorems [trans] = order_trans; (* <= <= <= *) |
|
40 |
theorems [trans] = order_antisym; (* <= >= = *) |
|
6862 | 41 |
|
7202 | 42 |
theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) |
7381 | 43 |
by (rule subst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
44 |
|
7202 | 45 |
theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) |
7381 | 46 |
by (rule ssubst); |
6862 | 47 |
|
7202 | 48 |
theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) |
7381 | 49 |
by (rule subst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
50 |
|
7202 | 51 |
theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
7381 | 52 |
by (rule ssubst); |
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
53 |
|
7381 | 54 |
theorems [trans] = trans (* = = = *) |
6945 | 55 |
|
8229 | 56 |
theorems [elim??] = sym |
57 |
||
6779
2912aff958bd
Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff
changeset
|
58 |
|
6862 | 59 |
end; |