summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 01 Jul 1999 17:42:27 +0200 | |

changeset 6873 | b123f5522ea1 |

parent 6872 | b250da153b1e |

child 6874 | 747f656e04ec |

tuned;

--- a/src/HOL/Calculation.thy Thu Jul 01 17:41:16 1999 +0200 +++ b/src/HOL/Calculation.thy Thu Jul 01 17:42:27 1999 +0200 @@ -2,33 +2,34 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Setup transitivity rules for calculational proofs. +Setup transitivity rules for calculational proofs. Note that in the +list below later rules have priority. *) theory Calculation = Int:; -theorems [trans] = Ord.order_antisym; (* <= <= = *) -theorems [trans] = Ord.order_trans; (* <= <= <= *) +theorems [trans] = HOL.ssubst; (* = x x *) +theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *) + +theorems [trans] = Divides.dvd_trans; (* dvd dvd dvd *) + theorems [trans] = Ord.order_less_trans; (* < < < *) theorems [trans] = Ord.order_le_less_trans; (* <= < < *) theorems [trans] = Ord.order_less_le_trans; (* < <= < *) +theorems [trans] = Ord.order_trans; (* <= <= <= *) +theorems [trans] = Ord.order_antisym; (* <= <= = *) theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) - by (rule HOL.subst[with y z]); + by (rule HOL.subst); theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) - by (rule HOL.ssubst[with x y]); + by (rule HOL.ssubst); theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) - by (rule HOL.subst[with y z]); + by (rule HOL.subst); theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) - by (rule HOL.ssubst[with x y]); - -theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *) -theorems [trans] = HOL.ssubst; (* = x x *) - -theorems [trans] = Divides.dvd_trans; (* dvd dvd dvd *) + by (rule HOL.ssubst); end;