1 (* Title: ZF/Rel.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Relations in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 (*** Some properties of relations -- useful? ***) |
|
10 |
|
11 (* irreflexivity *) |
|
12 |
|
13 val prems = Goalw [irrefl_def] |
|
14 "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)"; |
|
15 by (REPEAT (ares_tac (prems @ [ballI]) 1)); |
|
16 qed "irreflI"; |
|
17 |
|
18 Goalw [irrefl_def] "[| irrefl(A,r); x:A |] ==> <x,x> ~: r"; |
|
19 by (Blast_tac 1); |
|
20 qed "irreflE"; |
|
21 |
|
22 (* symmetry *) |
|
23 |
|
24 val prems = Goalw [sym_def] |
|
25 "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"; |
|
26 by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); |
|
27 qed "symI"; |
|
28 |
|
29 Goalw [sym_def] "[| sym(r); <x,y>: r |] ==> <y,x>: r"; |
|
30 by (Blast_tac 1); |
|
31 qed "symE"; |
|
32 |
|
33 (* antisymmetry *) |
|
34 |
|
35 val prems = Goalw [antisym_def] |
|
36 "[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> \ |
|
37 \ antisym(r)"; |
|
38 by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); |
|
39 qed "antisymI"; |
|
40 |
|
41 Goalw [antisym_def] "[| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y"; |
|
42 by (Blast_tac 1); |
|
43 qed "antisymE"; |
|
44 |
|
45 (* transitivity *) |
|
46 |
|
47 Goalw [trans_def] "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r"; |
|
48 by (Blast_tac 1); |
|
49 qed "transD"; |
|
50 |
|
51 Goalw [trans_on_def] |
|
52 "[| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r"; |
|
53 by (Blast_tac 1); |
|
54 qed "trans_onD"; |
|
55 |
|