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