src/ZF/ex/tf.ML
author nipkow
Mon, 06 Dec 1993 17:05:10 +0100
changeset 189 831a9a7ab9f3
parent 77 c94c8ebc0b15
child 279 7738aed3f84d
permissions -rw-r--r--
added rep_tsig
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ex/tf.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Trees & forests, a mutually recursive type definition.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
structure TF = Datatype_Fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
 (val thy = Univ.thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
  val rec_specs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
      [("tree", "univ(A)",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
	  [(["Tcons"],	"[i,i]=>i")]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
       ("forest", "univ(A)",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
	  [(["Fnil"],	"i"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
	   (["Fcons"],	"[i,i]=>i")])];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val rec_styp = "i=>i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val ext = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val sintrs = 
77
c94c8ebc0b15 ZF/ex/tf,tf_fn: renamed the variable tf to f everywhere
lcp
parents: 71
diff changeset
    20
	  ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
	   "Fnil : forest(A)",
77
c94c8ebc0b15 ZF/ex/tf,tf_fn: renamed the variable tf to f everywhere
lcp
parents: 71
diff changeset
    22
	   "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  val monos = [];
71
729fe026c5f3 sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents: 56
diff changeset
    24
  val type_intrs = datatype_intrs
729fe026c5f3 sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents: 56
diff changeset
    25
  val type_elims = datatype_elims);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val [TconsI, FnilI, FconsI] = TF.intrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
(** tree_forest(A) as the union of tree(A) and forest(A) **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
goalw TF.thy (tl TF.defs) "tree(A) <= tree_forest(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val tree_subset_TF = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
goalw TF.thy (tl TF.defs) "forest(A) <= tree_forest(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val forest_subset_TF = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
goalw TF.thy (tl TF.defs) "tree(A) Un forest(A) = tree_forest(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
by (rtac (TF.dom_subset RS Part_sum_equality) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val TF_equals_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(** NOT useful, but interesting... **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    45
(*The (refl RS conjI RS exI RS exI) avoids considerable search!*)
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    46
val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI]
71
729fe026c5f3 sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents: 56
diff changeset
    47
                    addIs datatype_intrs
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    48
                    addDs [TF.dom_subset RS subsetD]
71
729fe026c5f3 sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents: 56
diff changeset
    49
	            addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    50
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
by (rewrite_goals_tac TF.con_defs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
by (rtac equalityI 1);
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    55
by (fast_tac unfold_cs 1);
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    56
by (fast_tac unfold_cs 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val tree_unfold = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
by (rewrite_goals_tac TF.con_defs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (rtac equalityI 1);
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    63
by (fast_tac unfold_cs 1);
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 0
diff changeset
    64
by (fast_tac unfold_cs 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val forest_unfold = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66