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--
```     1 (*  Title:      HOL/Calculation.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Markus Wenzel, TU Muenchen
```
```     4
```
```     5 Setup transitivity rules for calculational proofs.  Note that in the
```
```     6 list below later rules have priority.
```
```     7 *)
```
```     8
```
```     9 theory Calculation = Int:;
```
```    10
```
```    11
```
```    12 theorem [trans]: "[| s = t; P t |] ==> P s"; 		    (*  =  x  x  *)
```
```    13   by (rule ssubst);
```
```    14
```
```    15 theorem [trans]: "[| P s; s = t |] ==> P t";		    (*  x  =  x  *)
```
```    16   by (rule subst);
```
```    17
```
```    18 theorems [trans] = dvd_trans;                               (* dvd dvd dvd *)
```
```    19
```
```    20 theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y";     (*  ~=  <=  < *)
```
```    21   by (simp! add: order_less_le);
```
```    22
```
```    23 theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y";     (*  <=  ~=  < *)
```
```    24   by (simp! add: order_less_le);
```
```    25
```
```    26 theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P";   (*  <  >  P  *)
```
```    27   by (rule order_less_asym);
```
```    28
```
```    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;                           (*  <= >= =  *)
```
```    34
```
```    35 theorem [trans]: "[| x <= y; y = z |] ==> x <= z";	    (*  <= =  <= *)
```
```    36   by (rule subst);
```
```    37
```
```    38 theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	    (*  =  <= <= *)
```
```    39   by (rule ssubst);
```
```    40
```
```    41 theorem [trans]: "[| x < y; y = z |] ==> x < z";	    (*  <  =  <  *)
```
```    42   by (rule subst);
```
```    43
```
```    44 theorem [trans]: "[| x = y; y < z |] ==> x < z";	    (*  =  <  <  *)
```
```    45   by (rule ssubst);
```
```    46
```
```    47 theorems [trans] = trans                                    (*  =  =  =  *)
```
```    48
```
```    49
```
```    50 end;
```