author wenzelm Sun, 25 Jun 2000 23:58:54 +0200 changeset 9142 d5a841f89e92 parent 9141 49f6e45e7199 child 9143 6180c29d2db6
prefer mp over subst; tuned;
 src/HOL/Calculation.thy file | annotate | diff | comparison | revisions
```--- 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"  (*  ~=  <=  < *)

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

-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
```