1 (* Title: HOL/ex/rel |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Domain, range of a relation or function -- NOT YET WORKING |
|
7 *) |
|
8 |
|
9 structure Rel = |
|
10 struct |
|
11 val thy = extend_theory Univ.thy "Rel" |
|
12 ([], [], [], [], |
|
13 [ |
|
14 (["domain"], "('a * 'b)set => 'a set"), |
|
15 (["range2"], "('a * 'b)set => 'b set"), |
|
16 (["field"], "('a * 'a)set => 'a set") |
|
17 ], |
|
18 None) |
|
19 [ |
|
20 ("domain_def", "domain(r) == {a. ? b. (a,b) : r}" ), |
|
21 ("range2_def", "range2(r) == {b. ? a. (a,b) : r}" ), |
|
22 ("field_def", "field(r) == domain(r) Un range2(r)" ) |
|
23 ]; |
|
24 end; |
|
25 |
|
26 local val ax = get_axiom Rel.thy |
|
27 in |
|
28 val domain_def = ax"domain_def"; |
|
29 val range2_def = ax"range2_def"; |
|
30 val field_def = ax"field_def"; |
|
31 end; |
|
32 |
|
33 |
|
34 (*** domain ***) |
|
35 |
|
36 val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)"; |
|
37 by (fast_tac (claset() addIs [prem]) 1); |
|
38 qed "domainI"; |
|
39 |
|
40 val major::prems = goalw Rel.thy [domain_def] |
|
41 "[| a : domain(r); !!y. (a,y): r ==> P |] ==> P"; |
|
42 by (rtac (major RS CollectE) 1); |
|
43 by (etac exE 1); |
|
44 by (REPEAT (ares_tac prems 1)); |
|
45 qed "domainE"; |
|
46 |
|
47 |
|
48 (*** range2 ***) |
|
49 |
|
50 val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)"; |
|
51 by (fast_tac (claset() addIs [prem]) 1); |
|
52 qed "range2I"; |
|
53 |
|
54 val major::prems = goalw Rel.thy [range2_def] |
|
55 "[| b : range2(r); !!x. (x,b): r ==> P |] ==> P"; |
|
56 by (rtac (major RS CollectE) 1); |
|
57 by (etac exE 1); |
|
58 by (REPEAT (ares_tac prems 1)); |
|
59 qed "range2E"; |
|
60 |
|
61 |
|
62 (*** field ***) |
|
63 |
|
64 val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> a : field(r)"; |
|
65 by (rtac (prem RS domainI RS UnI1) 1); |
|
66 qed "fieldI1"; |
|
67 |
|
68 val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> b : field(r)"; |
|
69 by (rtac (prem RS range2I RS UnI2) 1); |
|
70 qed "fieldI2"; |
|
71 |
|
72 val [prem] = goalw Rel.thy [field_def] |
|
73 "(~ (c,a):r ==> (a,b): r) ==> a : field(r)"; |
|
74 by (rtac (prem RS domainI RS UnCI) 1); |
|
75 by (swap_res_tac [range2I] 1); |
|
76 by (etac notnotD 1); |
|
77 qed "fieldCI"; |
|
78 |
|
79 val major::prems = goalw Rel.thy [field_def] |
|
80 "[| a : field(r); \ |
|
81 \ !!x. (a,x): r ==> P; \ |
|
82 \ !!x. (x,a): r ==> P |] ==> P"; |
|
83 by (rtac (major RS UnE) 1); |
|
84 by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1)); |
|
85 qed "fieldE"; |
|
86 |
|
87 goalw Rel.thy [field_def] "domain(r) <= field(r)"; |
|
88 by (rtac Un_upper1 1); |
|
89 qed "domain_in_field"; |
|
90 |
|
91 goalw Rel.thy [field_def] "range2(r) <= field(r)"; |
|
92 by (rtac Un_upper2 1); |
|
93 qed "range2_in_field"; |
|
94 |
|
95 |
|
96 ????????????????????????????????????????????????????????????????; |
|
97 |
|
98 (*If r allows well-founded induction then wf(r)*) |
|
99 val [prem1,prem2] = goalw Rel.thy [wf_def] |
|
100 "[| field(r)<=A; \ |
|
101 \ !!P u. ! x:A. (! y. (y,x): r --> P(y)) --> P(x) ==> P(u) |] \ |
|
102 \ ==> wf(r)"; |
|
103 by (rtac (prem1 RS wfI) 1); |
|
104 by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1); |
|
105 by (Fast_tac 3); |
|
106 by (Fast_tac 2); |
|
107 by (Fast_tac 1); |
|
108 qed "wfI2"; |
|
109 |
|