isabelle: src/HOL/Calculation.thy@747f656e04ec (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
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	11	theorems [trans] = HOL.ssubst; (* = x x *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	12	theorems [trans] = HOL.subst[COMP swap_prems_rl]; (* x = x *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	13
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	14	theorems [trans] = Divides.dvd_trans; (* dvd dvd dvd *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	15
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	16	theorems [trans] = Ord.order_less_trans; (* < < < *)
f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	17	theorems [trans] = Ord.order_le_less_trans; (* <= < < *)
f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	18	theorems [trans] = Ord.order_less_le_trans; (* < <= < *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	19	theorems [trans] = Ord.order_trans; (* <= <= <= *)
b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	20	theorems [trans] = Ord.order_antisym; (* <= <= = *)
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	21
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	22	theorem [trans]: "[\| x <= y; y = z \|] ==> x <= z"; (* <= = <= *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	23	by (rule HOL.subst);
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	24
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	25	theorem [trans]: "[\| x = y; y <= z \|] ==> x <= z"; (* = <= <= *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	26	by (rule HOL.ssubst);
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	27
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	28	theorem [trans]: "[\| x < y; y = z \|] ==> x < z"; (* < = < *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	29	by (rule HOL.subst);
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	30
6863 6c8bf18f9da9 antisym first; wenzelm parents: 6862 diff changeset	31	theorem [trans]: "[\| x = y; y < z \|] ==> x < z"; (* = < < *)
6873 b123f5522ea1 tuned; wenzelm parents: 6863 diff changeset	32	by (rule HOL.ssubst);
6779 2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	33
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs. wenzelm parents: diff changeset	34
6862 f80091bdc992 more robust trans rules; wenzelm parents: 6791 diff changeset	35	end;

author	wenzelm
	Thu, 01 Jul 1999 21:19:45 +0200
changeset 6874	747f656e04ec
parent 6873	b123f5522ea1
child 6945	eeeef70c8fe3
permissions	-rw-r--r--