src/ZF/ex/tf.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/tf.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Trees & forests, a mutually recursive type definition.
     7 *)
     8 
     9 structure TF = Datatype_Fun
    10  (val thy        = Univ.thy
    11   val rec_specs  = [("tree", "univ(A)",
    12                        [(["Tcons"],  "[i,i]=>i")]),
    13                     ("forest", "univ(A)",
    14                        [(["Fnil"],   "i"),
    15                         (["Fcons"],  "[i,i]=>i")])]
    16   val rec_styp   = "i=>i"
    17   val ext        = None
    18   val sintrs     = 
    19           ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
    20            "Fnil : forest(A)",
    21            "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
    22   val monos      = []
    23   val type_intrs = datatype_intrs
    24   val type_elims = datatype_elims);
    25 
    26 val [TconsI, FnilI, FconsI] = TF.intrs;
    27 
    28 (** tree_forest(A) as the union of tree(A) and forest(A) **)
    29 
    30 goalw TF.thy (tl TF.defs) "tree(A) <= tree_forest(A)";
    31 by (rtac Part_subset 1);
    32 val tree_subset_TF = result();
    33 
    34 goalw TF.thy (tl TF.defs) "forest(A) <= tree_forest(A)";
    35 by (rtac Part_subset 1);
    36 val forest_subset_TF = result();
    37 
    38 goalw TF.thy (tl TF.defs) "tree(A) Un forest(A) = tree_forest(A)";
    39 by (rtac (TF.dom_subset RS Part_sum_equality) 1);
    40 val TF_equals_Un = result();
    41 
    42 (** NOT useful, but interesting... **)
    43 
    44 (*The (refl RS conjI RS exI RS exI) avoids considerable search!*)
    45 val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI]
    46                     addIs datatype_intrs
    47                     addDs [TF.dom_subset RS subsetD]
    48 	            addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
    49 
    50 goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
    51 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
    52 by (rewrite_goals_tac TF.con_defs);
    53 by (rtac equalityI 1);
    54 by (fast_tac unfold_cs 1);
    55 by (fast_tac unfold_cs 1);
    56 val tree_unfold = result();
    57 
    58 goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
    59 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
    60 by (rewrite_goals_tac TF.con_defs);
    61 by (rtac equalityI 1);
    62 by (fast_tac unfold_cs 1);
    63 by (fast_tac unfold_cs 1);
    64 val forest_unfold = result();
    65