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