isabelle: src/ZF/Rel.ML@a3b73ba44a11 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 760 diff changeset	1	(* Title: ZF/Rel.ML
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 760 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	5
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	6	For Rel.thy. Relations in Zermelo-Fraenkel Set Theory
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	7	*)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	8
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	9	open Rel;
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	10
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	11	(* Some properties of relations -- useful? *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	12
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	13	(* irreflexivity *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	14
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	15	val prems = goalw Rel.thy [irrefl_def]
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	16	"[\| !!x. x:A ==> <x,x> ~: r \|] ==> irrefl(A,r)";
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	17	by (REPEAT (ares_tac (prems @ [ballI]) 1));
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	18	qed "irreflI";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	19
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	20	val prems = goalw Rel.thy [irrefl_def]
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	21	"[\| irrefl(A,r); x:A \|] ==> <x,x> ~: r";
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	22	by (rtac (prems MRS bspec) 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	23	qed "irreflE";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	24
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	25	(* symmetry *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	26
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	27	val prems = goalw Rel.thy [sym_def]
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	28	"[\| !!x y.<x,y>: r ==> <y,x>: r \|] ==> sym(r)";
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	29	by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	30	qed "symI";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	31
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	32	goalw Rel.thy [sym_def] "!!r. [\| sym(r); <x,y>: r \|] ==> <y,x>: r";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	33	by (Fast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	34	qed "symE";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	35
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	36	(* antisymmetry *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	37
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	38	val prems = goalw Rel.thy [antisym_def]
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	39	"[\| !!x y.[\| <x,y>: r; <y,x>: r \|] ==> x=y \|] ==> \
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	40	\ antisym(r)";
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	41	by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	42	qed "antisymI";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	43
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	44	val prems = goalw Rel.thy [antisym_def]
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	45	"!!r. [\| antisym(r); <x,y>: r; <y,x>: r \|] ==> x=y";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	46	by (Fast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	47	qed "antisymE";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	48
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	49	(* transitivity *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	50
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	51	goalw Rel.thy [trans_def]
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	52	"!!r. [\| trans(r); <a,b>:r; <b,c>:r \|] ==> <a,c>:r";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	53	by (Fast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	54	qed "transD";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	55
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	56	goalw Rel.thy [trans_on_def]
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	57	"!!r. [\| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A \|] ==> <a,c>:r";
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1461 diff changeset	58	by (Fast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	59	qed "trans_onD";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	60

author	nipkow
	Wed, 23 Apr 1997 09:14:56 +0200
changeset 3011	a3b73ba44a11
parent 2469	b50b8c0eec01
child 3016	15763781afb0
permissions	-rw-r--r--