isabelle: src/ZF/Rel.ML@825877190618 (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
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5137 diff changeset	6	Relations in Zermelo-Fraenkel Set Theory
435 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
5137 60205b0de9b9 Huge tidy-up: removal of leading \!\! paulson parents: 5067 diff changeset	32	Goalw [sym_def] "[\| sym(r); <x,y>: r \|] ==> <y,x>: r";
3016 15763781afb0 Conversion to use blast_tac paulson parents: 2469 diff changeset	33	by (Blast_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";
3016 15763781afb0 Conversion to use blast_tac paulson parents: 2469 diff changeset	46	by (Blast_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
5067 62b6288e6005 isatool fixgoal; wenzelm parents: 3016 diff changeset	51	Goalw [trans_def]
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5137 diff changeset	52	"[\| trans(r); <a,b>:r; <b,c>:r \|] ==> <a,c>:r";
3016 15763781afb0 Conversion to use blast_tac paulson parents: 2469 diff changeset	53	by (Blast_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
5067 62b6288e6005 isatool fixgoal; wenzelm parents: 3016 diff changeset	56	Goalw [trans_on_def]
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5137 diff changeset	57	"[\| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A \|] ==> <a,c>:r";
3016 15763781afb0 Conversion to use blast_tac paulson parents: 2469 diff changeset	58	by (Blast_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	paulson
	Wed, 15 Jul 1998 14:13:18 +0200
changeset 5147	825877190618
parent 5137	60205b0de9b9
child 5321	f8848433d240
permissions	-rw-r--r--