isabelle: src/ZF/Rel.ML@fcd29e58c40c (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	(* Some properties of relations -- useful? *)
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	(* irreflexivity *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	12
5321 f8848433d240 got rid of some goal thy commands paulson parents: 5147 diff changeset	13	val prems = Goalw [irrefl_def]
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	14	"[\| !!x. x:A ==> <x,x> ~: r \|] ==> irrefl(A,r)";
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	15	by (REPEAT (ares_tac (prems @ [ballI]) 1));
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	16	qed "irreflI";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	17
5321 f8848433d240 got rid of some goal thy commands paulson parents: 5147 diff changeset	18	Goalw [irrefl_def] "[\| irrefl(A,r); x:A \|] ==> <x,x> ~: r";
f8848433d240 got rid of some goal thy commands paulson parents: 5147 diff changeset	19	by (Blast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	20	qed "irreflE";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	21
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	22	(* symmetry *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	23
5321 f8848433d240 got rid of some goal thy commands paulson parents: 5147 diff changeset	24	val prems = Goalw [sym_def]
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	25	"[\| !!x y.<x,y>: r ==> <y,x>: r \|] ==> sym(r)";
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	26	by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	27	qed "symI";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	28
5137 60205b0de9b9 Huge tidy-up: removal of leading \!\! paulson parents: 5067 diff changeset	29	Goalw [sym_def] "[\| sym(r); <x,y>: r \|] ==> <y,x>: r";
3016 15763781afb0 Conversion to use blast_tac paulson parents: 2469 diff changeset	30	by (Blast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	31	qed "symE";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	32
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	33	(* antisymmetry *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	34
5321 f8848433d240 got rid of some goal thy commands paulson parents: 5147 diff changeset	35	val prems = Goalw [antisym_def]
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	36	"[\| !!x y.[\| <x,y>: r; <y,x>: r \|] ==> x=y \|] ==> \
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	37	\ antisym(r)";
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	38	by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	39	qed "antisymI";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	40
5321 f8848433d240 got rid of some goal thy commands paulson parents: 5147 diff changeset	41	Goalw [antisym_def] "[\| antisym(r); <x,y>: r; <y,x>: r \|] ==> x=y";
3016 15763781afb0 Conversion to use blast_tac paulson parents: 2469 diff changeset	42	by (Blast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	43	qed "antisymE";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	44
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	45	(* transitivity *)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	46
5321 f8848433d240 got rid of some goal thy commands paulson parents: 5147 diff changeset	47	Goalw [trans_def] "[\| trans(r); <a,b>:r; <b,c>:r \|] ==> <a,c>:r";
3016 15763781afb0 Conversion to use blast_tac paulson parents: 2469 diff changeset	48	by (Blast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	49	qed "transD";
435 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_on_def]
5147 825877190618 More tidying and removal of "\!\!... from Goal commands paulson parents: 5137 diff changeset	52	"[\| 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	53	by (Blast_tac 1);
760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 435 diff changeset	54	qed "trans_onD";
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	55

author	wenzelm
	Fri, 01 Dec 2000 19:39:54 +0100
changeset 10562	fcd29e58c40c
parent 9907	473a6604da94
permissions	-rw-r--r--