src/ZF/ex/acc.ML
author nipkow
Mon, 06 Dec 1993 17:05:10 +0100
changeset 189 831a9a7ab9f3
parent 95 2246a80b1cb5
child 279 7738aed3f84d
permissions -rw-r--r--
added rep_tsig
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ex/acc
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Inductive definition of acc(r)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
structure Acc = Inductive_Fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
 (val thy = WF.thy addconsts [(["acc"],"i=>i")];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val rec_doms = [("acc", "field(r)")];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val sintrs = 
95
2246a80b1cb5 Minor changes; addition of counit.ML
lcp
parents: 0
diff changeset
    16
      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val monos = [Pow_mono];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val con_defs = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val type_intrs = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val type_elims = []);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
by (etac Acc.elim 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
val acc_downward = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val [major] = goal Acc.thy "field(r) <= acc(r) ==> wf(r)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
by (rtac (major RS wfI2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (etac Acc.induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
by (etac (bspec RS mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
by (resolve_tac Acc.intrs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
by (assume_tac 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
by (ALLGOALS (fast_tac ZF_cs));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
val acc_wfI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
goal ZF.thy "!!r A. field(r Int A*A) <= field(r) Int A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val field_Int_prodself = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
goal Acc.thy "wf(r Int (acc(r)*acc(r)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (rtac (field_Int_prodself RS wfI2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (etac IntE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (etac Acc.induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
by (etac (bspec RS mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
by (rtac IntI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (resolve_tac Acc.intrs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (assume_tac 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
by (ALLGOALS (fast_tac ZF_cs));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
val wf_acc_Int = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (etac (major RS wf_induct2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by (rtac subset_refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
by (resolve_tac Acc.intrs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
by (assume_tac 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val acc_wfD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
goal Acc.thy "wf(r) <-> field(r) <= acc(r)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val wf_acc_iff = result();