src/ZF/ex/Data.ML
author lcp
Mon, 01 Aug 1994 17:34:57 +0200
changeset 503 15375d7b379c
parent 486 6b58082796f6
child 515 abcc438e7c27
permissions -rw-r--r--
trivial whitespace change
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/ex/data.ML
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     2
    ID:         $Id$
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     5
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     6
Sample datatype definition.  
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     7
It has four contructors, of arities 0-3, and two parameters A and B.
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     8
*)
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
     9
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    10
structure Data = Datatype_Fun
279
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    11
 (val thy        = Univ.thy
503
15375d7b379c trivial whitespace change
lcp
parents: 486
diff changeset
    12
  val thy_name 	 = "Data"
279
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    13
  val rec_specs  = [("data", "univ(A Un B)",
486
6b58082796f6 Misc minor updates
lcp
parents: 477
diff changeset
    14
                       [(["Con0"],   "i",	    NoSyn),
6b58082796f6 Misc minor updates
lcp
parents: 477
diff changeset
    15
                        (["Con1"],   "i=>i",	    NoSyn),
6b58082796f6 Misc minor updates
lcp
parents: 477
diff changeset
    16
                        (["Con2"],   "[i,i]=>i",    NoSyn),
6b58082796f6 Misc minor updates
lcp
parents: 477
diff changeset
    17
                        (["Con3"],   "[i,i,i]=>i",  NoSyn)])]
279
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    18
  val rec_styp   = "[i,i]=>i"
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    19
  val sintrs     = 
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    20
          ["Con0 : data(A,B)",
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    21
           "[| a: A |] ==> Con1(a) : data(A,B)",
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    22
           "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    23
           "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
7738aed3f84d Improved layout for inductive defs
lcp
parents: 85
diff changeset
    24
  val monos      = []
71
729fe026c5f3 sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents: 56
diff changeset
    25
  val type_intrs = datatype_intrs
729fe026c5f3 sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents: 56
diff changeset
    26
  val type_elims = datatype_elims);
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    27
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    28
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    29
(**  Lemmas to justify using "data" in other recursive type definitions **)
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    30
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    31
goalw Data.thy Data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    32
by (rtac lfp_mono 1);
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    33
by (REPEAT (rtac Data.bnd_mono 1));
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    34
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    35
val data_mono = result();
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    36
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    37
goalw Data.thy (Data.defs@Data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    38
by (rtac lfp_lowerbound 1);
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    39
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    40
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    41
			    Pair_in_univ]) 1);
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    42
val data_univ = result();
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    43
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    44
val data_subset_univ = standard ([data_mono, data_univ] MRS subset_trans);
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    45
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents:
diff changeset
    46