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