1 (* Title: ZF/ex/acc |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Inductive definition of acc(r) |
|
7 |
|
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
|
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
|
10 *) |
|
11 |
|
12 (*The introduction rule must require a \\<in> field(r) |
|
13 Otherwise acc(r) would be a proper class! *) |
|
14 |
|
15 (*The intended introduction rule*) |
|
16 val prems = goal Acc.thy |
|
17 "[| !!b. <b,a>:r ==> b \\<in> acc(r); a \\<in> field(r) |] ==> a \\<in> acc(r)"; |
|
18 by (fast_tac (claset() addIs prems@acc.intrs) 1); |
|
19 qed "accI"; |
|
20 |
|
21 Goal "[| b \\<in> acc(r); <a,b>: r |] ==> a \\<in> acc(r)"; |
|
22 by (etac acc.elim 1); |
|
23 by (Fast_tac 1); |
|
24 qed "acc_downward"; |
|
25 |
|
26 val [major,indhyp] = goal Acc.thy |
|
27 "[| a \\<in> acc(r); \ |
|
28 \ !!x. [| x \\<in> acc(r); \\<forall>y. <y,x>:r --> P(y) |] ==> P(x) \ |
|
29 \ |] ==> P(a)"; |
|
30 by (rtac (major RS acc.induct) 1); |
|
31 by (rtac indhyp 1); |
|
32 by (Fast_tac 2); |
|
33 by (resolve_tac acc.intrs 1); |
|
34 by (assume_tac 2); |
|
35 by (etac (Collect_subset RS Pow_mono RS subsetD) 1); |
|
36 qed "acc_induct"; |
|
37 |
|
38 Goal "wf[acc(r)](r)"; |
|
39 by (rtac wf_onI2 1); |
|
40 by (etac acc_induct 1); |
|
41 by (Fast_tac 1); |
|
42 qed "wf_on_acc"; |
|
43 |
|
44 (* field(r) \\<subseteq> acc(r) ==> wf(r) *) |
|
45 val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf; |
|
46 |
|
47 val [major] = goal Acc.thy "wf(r) ==> field(r) \\<subseteq> acc(r)"; |
|
48 by (rtac subsetI 1); |
|
49 by (etac (major RS wf_induct2) 1); |
|
50 by (rtac subset_refl 1); |
|
51 by (rtac accI 1); |
|
52 by (assume_tac 2); |
|
53 by (Fast_tac 1); |
|
54 qed "acc_wfD"; |
|
55 |
|
56 Goal "wf(r) <-> field(r) \\<subseteq> acc(r)"; |
|
57 by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); |
|
58 qed "wf_acc_iff"; |
|