isabelle: src/HOL/Calculation.thy@601f930d3739 (annotated)

6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	1	(* Title: HOL/Calculation.thy
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	2	ID: $Id$
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	3	Author: Markus Wenzel, TU Muenchen
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	4
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	5	Setup transitivity rules for calculational proofs. Note that in the
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	6	list below later rules have priority.
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	7	*)
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	8
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	9	theory Calculation = Int:;
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	10
6945 eeeef70c8fe3 added HOL.trans; wenzelm parents: 6873 diff changeset	11
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	12	theorems [trans] = HOL.ssubst; (* = x x *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	13	theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	14
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	15	theorems [trans] = Divides.dvd_trans; (* dvd dvd dvd *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	16
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	17	theorems [trans] = Ord.order_less_trans; (* < < < *)
f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	18	theorems [trans] = Ord.order_le_less_trans; (* <= < < *)
f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	19	theorems [trans] = Ord.order_less_le_trans; (* < <= < *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	20	theorems [trans] = Ord.order_trans; (* <= <= <= *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	21	theorems [trans] = Ord.order_antisym; (* <= <= = *)
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	22
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	23	theorem [trans]: "[\| x <= y; y = z \|] ==> x <= z"; (* <= = <= *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	24	by (rule HOL.subst);
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	25
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	26	theorem [trans]: "[\| x = y; y <= z \|] ==> x <= z"; (* = <= <= *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	27	by (rule HOL.ssubst);
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	28
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	29	theorem [trans]: "[\| x < y; y = z \|] ==> x < z"; (* < = < *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	30	by (rule HOL.subst);
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	31
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	32	theorem [trans]: "[\| x = y; y < z \|] ==> x < z"; (* = < < *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	33	by (rule HOL.ssubst);
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	34
6945 eeeef70c8fe3 added HOL.trans; wenzelm parents: 6873 diff changeset	35	theorems [trans] = HOL.trans (* = = = *)
eeeef70c8fe3 added HOL.trans; wenzelm parents: 6873 diff changeset	36
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	37
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	38	end;

author	wenzelm
	Fri, 23 Jul 1999 16:50:55 +0200
changeset 7067	601f930d3739
parent 6945	eeeef70c8fe3
child 7202	6fcaf006cc40
permissions	-rw-r--r--