src/ZF/ex/bt.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 71 729fe026c5f3
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/bt.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Datatype definition of binary trees
     7 *)
     8 
     9 structure BT = Datatype_Fun
    10  (val thy = Univ.thy;
    11   val rec_specs = 
    12       [("bt", "univ(A)",
    13 	  [(["Lf"],"i"), (["Br"],"[i,i,i]=>i")])];
    14   val rec_styp = "i=>i";
    15   val ext = None
    16   val sintrs = 
    17 	  ["Lf : bt(A)",
    18 	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
    19   val monos = [];
    20   val type_intrs = datatype_intrs
    21   val type_elims = []);
    22 
    23 val [LfI, BrI] = BT.intrs;
    24 
    25 (*Perform induction on l, then prove the major premise using prems. *)
    26 fun bt_ind_tac a prems i = 
    27     EVERY [res_inst_tac [("x",a)] BT.induct i,
    28 	   rename_last_tac a ["1","2"] (i+2),
    29 	   ares_tac prems i];
    30 
    31 
    32 (**  Lemmas to justify using "bt" in other recursive type definitions **)
    33 
    34 goalw BT.thy BT.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
    35 by (rtac lfp_mono 1);
    36 by (REPEAT (rtac BT.bnd_mono 1));
    37 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
    38 val bt_mono = result();
    39 
    40 goalw BT.thy (BT.defs@BT.con_defs) "bt(univ(A)) <= univ(A)";
    41 by (rtac lfp_lowerbound 1);
    42 by (rtac (A_subset_univ RS univ_mono) 2);
    43 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
    44 			    Pair_in_univ]) 1);
    45 val bt_univ = result();
    46 
    47 val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
    48