Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Calculation.thy
author wenzelm
Wed, 30 Jun 1999 13:42:47 +0200
changeset 6862 f80091bdc992
parent 6791 2be411437c60
child 6863 6c8bf18f9da9
permissions -rw-r--r--
more robust trans rules;

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

Setup transitivity rules for calculational proofs.
*)

theory Calculation = Int:;

theorems [trans] = Ord.order_trans;                     (*  <= <= <= *)
theorems [trans] = Ord.order_less_trans;                (*  <  <  <  *)
theorems [trans] = Ord.order_le_less_trans;             (*  <= <  <  *)
theorems [trans] = Ord.order_less_le_trans;             (*  <  <= <  *)
theorems [trans] = Ord.order_antisym;                   (*  <= <= =  *)

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

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

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

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

theorems [trans] = HOL.subst[COMP swap_prems_rl];       (*  x  =  x  *)
theorems [trans] = HOL.ssubst;                          (*  =  x  x  *)

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


end;
isabelle