src/ZF/ex/Acc.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 782 200a16083201
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
clasohm@0
     1
(*  Title: 	ZF/ex/acc
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Inductive definition of acc(r)
clasohm@0
     7
clasohm@0
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
clasohm@0
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
clasohm@0
    10
*)
clasohm@0
    11
lcp@515
    12
open Acc;
clasohm@0
    13
lcp@434
    14
(*The introduction rule must require  a:field(r)  
lcp@434
    15
  Otherwise acc(r) would be a proper class!    *)
lcp@434
    16
lcp@515
    17
(*The intended introduction rule*)
lcp@515
    18
val prems = goal Acc.thy
lcp@515
    19
    "[| !!b. <b,a>:r ==> b: acc(r);  a: field(r) |] ==> a: acc(r)";
lcp@515
    20
by (fast_tac (ZF_cs addIs (prems@acc.intrs)) 1);
lcp@515
    21
val accI = result();
lcp@515
    22
clasohm@0
    23
goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
lcp@515
    24
by (etac acc.elim 1);
clasohm@0
    25
by (fast_tac ZF_cs 1);
clasohm@0
    26
val acc_downward = result();
clasohm@0
    27
lcp@434
    28
val [major,indhyp] = goal Acc.thy
lcp@434
    29
    "[| a : acc(r);						\
lcp@434
    30
\       !!x. [| x: acc(r);  ALL y. <y,x>:r --> P(y) |] ==> P(x)	\
lcp@434
    31
\    |] ==> P(a)";
lcp@515
    32
by (rtac (major RS acc.induct) 1);
lcp@438
    33
by (rtac indhyp 1);
lcp@434
    34
by (fast_tac ZF_cs 2);
lcp@515
    35
by (resolve_tac acc.intrs 1);
lcp@438
    36
by (assume_tac 2);
lcp@515
    37
be (Collect_subset RS Pow_mono RS subsetD) 1;
lcp@434
    38
val acc_induct = result();
clasohm@0
    39
lcp@434
    40
goal Acc.thy "wf[acc(r)](r)";
lcp@438
    41
by (rtac wf_onI2 1);
lcp@438
    42
by (etac acc_induct 1);
lcp@434
    43
by (fast_tac ZF_cs 1);
lcp@434
    44
val wf_on_acc = result();
lcp@434
    45
lcp@434
    46
(* field(r) <= acc(r) ==> wf(r) *)
lcp@434
    47
val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf;
clasohm@0
    48
clasohm@0
    49
val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)";
clasohm@0
    50
by (rtac subsetI 1);
clasohm@0
    51
by (etac (major RS wf_induct2) 1);
clasohm@0
    52
by (rtac subset_refl 1);
lcp@515
    53
by (resolve_tac [accI] 1);
clasohm@0
    54
by (assume_tac 2);
clasohm@0
    55
by (fast_tac ZF_cs 1);
clasohm@0
    56
val acc_wfD = result();
clasohm@0
    57
clasohm@0
    58
goal Acc.thy "wf(r) <-> field(r) <= acc(r)";
clasohm@0
    59
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
clasohm@0
    60
val wf_acc_iff = result();