src/ZF/ex/acc.ML
author lcp
Thu Mar 17 12:36:58 1994 +0100 (1994-03-17)
changeset 279 7738aed3f84d
parent 95 2246a80b1cb5
permissions -rw-r--r--
Improved layout for inductive defs
     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     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
    16   val monos      = [Pow_mono]
    17   val con_defs   = []
    18   val type_intrs = []
    19   val type_elims = []);
    20 
    21 goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
    22 by (etac Acc.elim 1);
    23 by (fast_tac ZF_cs 1);
    24 val acc_downward = result();
    25 
    26 val [major] = goal Acc.thy "field(r) <= acc(r) ==> wf(r)";
    27 by (rtac (major RS wfI2) 1);
    28 by (rtac subsetI 1);
    29 by (etac Acc.induct 1);
    30 by (etac (bspec RS mp) 1);
    31 by (resolve_tac Acc.intrs 1);
    32 by (assume_tac 2);
    33 by (ALLGOALS (fast_tac ZF_cs));
    34 val acc_wfI = result();
    35 
    36 goal ZF.thy "!!r A. field(r Int A*A) <= field(r) Int A";
    37 by (fast_tac ZF_cs 1);
    38 val field_Int_prodself = result();
    39 
    40 goal Acc.thy "wf(r Int (acc(r)*acc(r)))";
    41 by (rtac (field_Int_prodself RS wfI2) 1);
    42 by (rtac subsetI 1);
    43 by (etac IntE 1);
    44 by (etac Acc.induct 1);
    45 by (etac (bspec RS mp) 1);
    46 by (rtac IntI 1);
    47 by (assume_tac 1);
    48 by (resolve_tac Acc.intrs 1);
    49 by (assume_tac 2);
    50 by (ALLGOALS (fast_tac ZF_cs));
    51 val wf_acc_Int = result();
    52 
    53 val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)";
    54 by (rtac subsetI 1);
    55 by (etac (major RS wf_induct2) 1);
    56 by (rtac subset_refl 1);
    57 by (resolve_tac Acc.intrs 1);
    58 by (assume_tac 2);
    59 by (fast_tac ZF_cs 1);
    60 val acc_wfD = result();
    61 
    62 goal Acc.thy "wf(r) <-> field(r) <= acc(r)";
    63 by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
    64 val wf_acc_iff = result();