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

author | wenzelm |

Mon, 09 Aug 1999 22:25:27 +0200 | |

changeset 7202 | 6fcaf006cc40 |

parent 7201 | 59b9b7aec3c5 |

child 7203 | 36990a7c7c72 |

added asym rule;

--- a/src/HOL/Calculation.thy Mon Aug 09 22:23:07 1999 +0200 +++ b/src/HOL/Calculation.thy Mon Aug 09 22:25:27 1999 +0200 @@ -9,30 +9,33 @@ theory Calculation = Int:; -theorems [trans] = HOL.ssubst; (* = x x *) -theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *) +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] = Divides.dvd_trans; (* dvd dvd dvd *) + +theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P"; (* < > P *) + by (rule Ord.order_less_asym); -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; (* <= <= = *) +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"; (* <= = <= *) +theorem [trans]: "[| x <= y; y = z |] ==> x <= z"; (* <= = <= *) by (rule HOL.subst); -theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) +theorem [trans]: "[| x = y; y <= z |] ==> x <= z"; (* = <= <= *) by (rule HOL.ssubst); -theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) +theorem [trans]: "[| x < y; y = z |] ==> x < z"; (* < = < *) by (rule HOL.subst); -theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) +theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) by (rule HOL.ssubst); -theorems [trans] = HOL.trans (* = = = *) +theorems [trans] = HOL.trans (* = = = *) end;