summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Calculation.thy

author | paulson |

Thu Sep 23 13:06:31 1999 +0200 (1999-09-23) | |

changeset 7584 | 5be4bb8e4e3f |

parent 7561 | ff8dbd0589aa |

child 7657 | dbbf7721126e |

permissions | -rw-r--r-- |

tidied; added lemma restrict_to_left

1 (* Title: HOL/Calculation.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

5 Setup transitivity rules for calculational proofs. Note that in the

6 list below later rules have priority.

7 *)

9 theory Calculation = Int:;

12 theorem [trans]: "[| s = t; P t |] ==> P s"; (* = x x *)

13 by (rule ssubst);

15 theorem [trans]: "[| P s; s = t |] ==> P t"; (* x = x *)

16 by (rule subst);

18 theorems [trans] = dvd_trans; (* dvd dvd dvd *)

20 theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y"; (* ~= <= < *)

21 by (simp! add: order_less_le);

23 theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y"; (* <= ~= < *)

24 by (simp! add: order_less_le);

26 theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"; (* < > P *)

27 by (rule order_less_asym);

29 theorems [trans] = order_less_trans; (* < < < *)

30 theorems [trans] = order_le_less_trans; (* <= < < *)

31 theorems [trans] = order_less_le_trans; (* < <= < *)

32 theorems [trans] = order_trans; (* <= <= <= *)

33 theorems [trans] = order_antisym; (* <= >= = *)

35 theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *)

36 by (rule subst);

38 theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *)

39 by (rule ssubst);

41 theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *)

42 by (rule subst);

44 theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *)

45 by (rule ssubst);

47 theorems [trans] = trans (* = = = *)

50 end;