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

author	paulson
	Wed, 25 Nov 1998 15:54:41 +0100
changeset 5971	c5a7a7685826
parent 5321	f8848433d240
child 9907	473a6604da94
permissions	-rw-r--r--