src/HOL/Calculation.thy

added split_eta_SetCompr2 (also to simpset), generalized SetCompr_Sigma_eq

(*  Title:      HOL/Calculation.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Setup transitivity rules for calculational proofs.  Note that in the
list below later rules have priority.
*)

theory Calculation = IntArith:;

theorems [trans] = rev_mp mp;

theorem [trans]: "[| s = t; P t |] ==> P s"; 		    (*  =  x  x  *)
  by (rule ssubst);

theorem [trans]: "[| P s; s = t |] ==> P t";		    (*  x  =  x  *)
  by (rule subst);

theorems [trans] = dvd_trans;                               (* dvd dvd dvd *)

theorem [trans]: "[| c:A; A <= B |] ==> c:B";
  by (rule subsetD);

theorem [trans]: "[| A <= B; c:A |] ==> c:B";
  by (rule subsetD);

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";     (*  <=  ~=  < *)
  by (simp! add: order_less_le);

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;                           (*  <= >= =  *)

theorem [trans]: "[| x <= y; y = z |] ==> x <= z";	    (*  <= =  <= *)
  by (rule subst);

theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	    (*  =  <= <= *)
  by (rule ssubst);

theorem [trans]: "[| x < y; y = z |] ==> x < z";	    (*  <  =  <  *)
  by (rule subst);

theorem [trans]: "[| x = y; y < z |] ==> x < z";	    (*  =  <  <  *)
  by (rule ssubst);

theorems [trans] = trans                                    (*  =  =  =  *)

theorems [elim??] = sym


end;