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
     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 open Acc;
    13 
    14 (*The introduction rule must require  a:field(r)  
    15   Otherwise acc(r) would be a proper class!    *)
    16 
    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 
    23 goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
    24 by (etac acc.elim 1);
    25 by (fast_tac ZF_cs 1);
    26 val acc_downward = result();
    27 
    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)";
    32 by (rtac (major RS acc.induct) 1);
    33 by (rtac indhyp 1);
    34 by (fast_tac ZF_cs 2);
    35 by (resolve_tac acc.intrs 1);
    36 by (assume_tac 2);
    37 be (Collect_subset RS Pow_mono RS subsetD) 1;
    38 val acc_induct = result();
    39 
    40 goal Acc.thy "wf[acc(r)](r)";
    41 by (rtac wf_onI2 1);
    42 by (etac acc_induct 1);
    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;
    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);
    53 by (resolve_tac [accI] 1);
    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();