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

author | wenzelm |

Sun, 25 Jun 2000 23:58:54 +0200 | |

changeset 9142 | d5a841f89e92 |

parent 9141 | 49f6e45e7199 |

child 9143 | 6180c29d2db6 |

prefer mp over subst;
tuned;

--- a/src/HOL/Calculation.thy Sun Jun 25 23:58:27 2000 +0200 +++ b/src/HOL/Calculation.thy Sun Jun 25 23:58:54 2000 +0200 @@ -8,15 +8,16 @@ theory Calculation = IntArith: -theorems [trans] = rev_mp mp - -theorem [trans]: "[| s = t; P t |] ==> P s" (* = x x *) +theorem [trans]: "[| s = t; P t |] ==> P s" (* = x x *) by (rule ssubst) -theorem [trans]: "[| P s; s = t |] ==> P t" (* x = x *) +theorem [trans]: "[| P s; s = t |] ==> P t" (* x = x *) by (rule subst) -theorems [trans] = dvd_trans (* dvd dvd dvd *) +theorems [trans] = rev_mp mp (* x --> x *) + (* --> x x *) + +theorems [trans] = dvd_trans (* dvd dvd dvd *) theorem [trans]: "[| c:A; A <= B |] ==> c:B" by (rule subsetD) @@ -24,34 +25,34 @@ theorem [trans]: "[| A <= B; c:A |] ==> c:B" by (rule subsetD) -theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y" (* ~= <= < *) +theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y" (* ~= <= < *) by (simp! add: order_less_le) -theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y" (* <= ~= < *) +theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y" (* <= ~= < *) by (simp! add: order_less_le) -theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P" (* < > P *) +theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P" (* < > P *) by (rule order_less_asym) -theorems [trans] = order_less_trans (* < < < *) -theorems [trans] = order_le_less_trans (* <= < < *) -theorems [trans] = order_less_le_trans (* < <= < *) -theorems [trans] = order_trans (* <= <= <= *) -theorems [trans] = order_antisym (* <= >= = *) +theorems [trans] = order_less_trans (* < < < *) +theorems [trans] = order_le_less_trans (* <= < < *) +theorems [trans] = order_less_le_trans (* < <= < *) +theorems [trans] = order_trans (* <= <= <= *) +theorems [trans] = order_antisym (* <= >= = *) -theorem [trans]: "[| x <= y; y = z |] ==> x <= z" (* <= = <= *) +theorem [trans]: "[| x <= y; y = z |] ==> x <= z" (* <= = <= *) by (rule subst) -theorem [trans]: "[| x = y; y <= z |] ==> x <= z" (* = <= <= *) +theorem [trans]: "[| x = y; y <= z |] ==> x <= z" (* = <= <= *) by (rule ssubst) -theorem [trans]: "[| x < y; y = z |] ==> x < z" (* < = < *) +theorem [trans]: "[| x < y; y = z |] ==> x < z" (* < = < *) by (rule subst) -theorem [trans]: "[| x = y; y < z |] ==> x < z" (* = < < *) +theorem [trans]: "[| x = y; y < z |] ==> x < z" (* = < < *) by (rule ssubst) -theorems [trans] = trans (* = = = *) +theorems [trans] = trans (* = = = *) theorems [elim??] = sym