src/ZF/ex/Acc.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 95 2246a80b1cb5
permissions -rw-r--r--
Initial revision
     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 structure Acc = Inductive_Fun
    13  (val thy = WF.thy addconsts [(["acc"],"i=>i")];
    14   val rec_doms = [("acc", "field(r)")];
    15   val sintrs = 
    16       ["[| r-``{b} : Pow(acc(r));  b : field(r) |] ==> b : acc(r)"];
    17   val monos = [Pow_mono];
    18   val con_defs = [];
    19   val type_intrs = [];
    20   val type_elims = []);
    21 
    22 goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
    23 by (etac Acc.elim 1);
    24 by (fast_tac ZF_cs 1);
    25 val acc_downward = result();
    26 
    27 val [major] = goal Acc.thy "field(r) <= acc(r) ==> wf(r)";
    28 by (rtac (major RS wfI2) 1);
    29 by (rtac subsetI 1);
    30 by (etac Acc.induct 1);
    31 by (etac (bspec RS mp) 1);
    32 by (resolve_tac Acc.intrs 1);
    33 by (assume_tac 2);
    34 by (ALLGOALS (fast_tac ZF_cs));
    35 val acc_wfI = result();
    36 
    37 goal ZF.thy "!!r A. field(r Int A*A) <= field(r) Int A";
    38 by (fast_tac ZF_cs 1);
    39 val field_Int_prodself = result();
    40 
    41 goal Acc.thy "wf(r Int (acc(r)*acc(r)))";
    42 by (rtac (field_Int_prodself RS wfI2) 1);
    43 by (rtac subsetI 1);
    44 by (etac IntE 1);
    45 by (etac Acc.induct 1);
    46 by (etac (bspec RS mp) 1);
    47 by (rtac IntI 1);
    48 by (assume_tac 1);
    49 by (resolve_tac Acc.intrs 1);
    50 by (assume_tac 2);
    51 by (ALLGOALS (fast_tac ZF_cs));
    52 val wf_acc_Int = result();
    53 
    54 val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)";
    55 by (rtac subsetI 1);
    56 by (etac (major RS wf_induct2) 1);
    57 by (rtac subset_refl 1);
    58 by (resolve_tac Acc.intrs 1);
    59 by (assume_tac 2);
    60 by (fast_tac ZF_cs 1);
    61 val acc_wfD = result();
    62 
    63 goal Acc.thy "wf(r) <-> field(r) <= acc(r)";
    64 by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
    65 val wf_acc_iff = result();