0
|
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 |
|
515
|
12 |
open Acc;
|
0
|
13 |
|
434
|
14 |
(*The introduction rule must require a:field(r)
|
|
15 |
Otherwise acc(r) would be a proper class! *)
|
|
16 |
|
515
|
17 |
(*The intended introduction rule*)
|
|
18 |
val prems = goal Acc.thy
|
|
19 |
"[| !!b. <b,a>:r ==> b: acc(r); a: field(r) |] ==> a: acc(r)";
|
|
20 |
by (fast_tac (ZF_cs addIs (prems@acc.intrs)) 1);
|
|
21 |
val accI = result();
|
|
22 |
|
0
|
23 |
goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)";
|
515
|
24 |
by (etac acc.elim 1);
|
0
|
25 |
by (fast_tac ZF_cs 1);
|
|
26 |
val acc_downward = result();
|
|
27 |
|
434
|
28 |
val [major,indhyp] = goal Acc.thy
|
|
29 |
"[| a : acc(r); \
|
|
30 |
\ !!x. [| x: acc(r); ALL y. <y,x>:r --> P(y) |] ==> P(x) \
|
|
31 |
\ |] ==> P(a)";
|
515
|
32 |
by (rtac (major RS acc.induct) 1);
|
438
|
33 |
by (rtac indhyp 1);
|
434
|
34 |
by (fast_tac ZF_cs 2);
|
515
|
35 |
by (resolve_tac acc.intrs 1);
|
438
|
36 |
by (assume_tac 2);
|
515
|
37 |
be (Collect_subset RS Pow_mono RS subsetD) 1;
|
434
|
38 |
val acc_induct = result();
|
0
|
39 |
|
434
|
40 |
goal Acc.thy "wf[acc(r)](r)";
|
438
|
41 |
by (rtac wf_onI2 1);
|
|
42 |
by (etac acc_induct 1);
|
434
|
43 |
by (fast_tac ZF_cs 1);
|
|
44 |
val wf_on_acc = result();
|
|
45 |
|
|
46 |
(* field(r) <= acc(r) ==> wf(r) *)
|
|
47 |
val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf;
|
0
|
48 |
|
|
49 |
val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)";
|
|
50 |
by (rtac subsetI 1);
|
|
51 |
by (etac (major RS wf_induct2) 1);
|
|
52 |
by (rtac subset_refl 1);
|
515
|
53 |
by (resolve_tac [accI] 1);
|
0
|
54 |
by (assume_tac 2);
|
|
55 |
by (fast_tac ZF_cs 1);
|
|
56 |
val acc_wfD = result();
|
|
57 |
|
|
58 |
goal Acc.thy "wf(r) <-> field(r) <= acc(r)";
|
|
59 |
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
|
|
60 |
val wf_acc_iff = result();
|