--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Data.ML Fri Oct 15 10:25:23 1993 +0100
@@ -0,0 +1,47 @@
+(* Title: ZF/ex/data.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Sample datatype definition.
+It has four contructors, of arities 0-3, and two parameters A and B.
+*)
+
+structure Data = Datatype_Fun
+ (val thy = Univ.thy;
+ val rec_specs =
+ [("data", "univ(A Un B)",
+ [(["Zero"], "i"),
+ (["One"], "i=>i"),
+ (["Two"], "[i,i]=>i"),
+ (["Three"], "[i,i,i]=>i")])];
+ val rec_styp = "[i,i]=>i";
+ val ext = None
+ val sintrs =
+ ["Zero : data(A,B)",
+ "[| a: A |] ==> One(a) : data(A,B)",
+ "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
+ "[| a: A; b: B; d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
+ val monos = [];
+ val type_intrs = data_typechecks
+ val type_elims = data_elims);
+
+
+(** Lemmas to justify using "data" in other recursive type definitions **)
+
+goalw Data.thy Data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
+by (rtac lfp_mono 1);
+by (REPEAT (rtac Data.bnd_mono 1));
+by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
+val data_mono = result();
+
+goalw Data.thy (Data.defs@Data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
+by (rtac lfp_lowerbound 1);
+by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
+by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
+ Pair_in_univ]) 1);
+val data_univ = result();
+
+val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
+
+