src/ZF/ex/Data.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 529 f0d16216e394
child 782 200a16083201
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp@515
     1
(*  Title: 	ZF/ex/Data.ML
lcp@56
     2
    ID:         $Id$
lcp@56
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@56
     4
    Copyright   1993  University of Cambridge
lcp@56
     5
lcp@56
     6
Sample datatype definition.  
lcp@56
     7
It has four contructors, of arities 0-3, and two parameters A and B.
lcp@56
     8
*)
lcp@56
     9
lcp@515
    10
open Data;
lcp@56
    11
lcp@515
    12
goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
lcp@529
    13
let open data;  val rew = rewrite_rule con_defs in  
lcp@529
    14
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
lcp@529
    15
                     addEs [rew elim]) 1)
lcp@529
    16
end;
lcp@515
    17
val data_unfold = result();
lcp@56
    18
lcp@56
    19
(**  Lemmas to justify using "data" in other recursive type definitions **)
lcp@56
    20
lcp@515
    21
goalw Data.thy data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
lcp@56
    22
by (rtac lfp_mono 1);
lcp@515
    23
by (REPEAT (rtac data.bnd_mono 1));
lcp@56
    24
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
lcp@56
    25
val data_mono = result();
lcp@56
    26
lcp@515
    27
goalw Data.thy (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
lcp@56
    28
by (rtac lfp_lowerbound 1);
lcp@56
    29
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
lcp@56
    30
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
lcp@56
    31
			    Pair_in_univ]) 1);
lcp@56
    32
val data_univ = result();
lcp@56
    33
lcp@56
    34
val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
lcp@56
    35
lcp@56
    36