author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8855  ef4848bb0696 
child 9035  371f023d3dbd 
permissions  rwrr 
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 

8855
ef4848bb0696
base on IntArith instead of Int (in order to leave out deleted simproc!);
wenzelm
parents:
8301
diff
changeset

9 
theory Calculation = IntArith:; 
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; 