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