src/ZF/ex/data.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
```     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 structure Data = Datatype_Fun
```
```    11  (val thy        = Univ.thy
```
```    12   val rec_specs  = [("data", "univ(A Un B)",
```
```    13                        [(["Con0"],   "i"),
```
```    14                         (["Con1"],   "i=>i"),
```
```    15                         (["Con2"],   "[i,i]=>i"),
```
```    16                         (["Con3"],   "[i,i,i]=>i")])]
```
```    17   val rec_styp   = "[i,i]=>i"
```
```    18   val ext        = None
```
```    19   val sintrs     =
```
```    20           ["Con0 : data(A,B)",
```
```    21            "[| a: A |] ==> Con1(a) : data(A,B)",
```
```    22            "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
```
```    23            "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
```
```    24   val monos      = []
```
```    25   val type_intrs = datatype_intrs
```
```    26   val type_elims = datatype_elims);
```
```    27
```
```    28
```
```    29 (**  Lemmas to justify using "data" in other recursive type definitions **)
```
```    30
```
```    31 goalw Data.thy Data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
```
```    32 by (rtac lfp_mono 1);
```
```    33 by (REPEAT (rtac Data.bnd_mono 1));
```
```    34 by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
```
```    35 val data_mono = result();
```
```    36
```
```    37 goalw Data.thy (Data.defs@Data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
```
```    38 by (rtac lfp_lowerbound 1);
```
```    39 by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
```
```    40 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
```
```    41 			    Pair_in_univ]) 1);
```
```    42 val data_univ = result();
```
```    43
```
```    44 val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
```
```    45
```
```    46
```