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
clasohm@0
     1
(*  Title: 	ZF/ex/bt.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
Datatype definition of binary trees
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
structure BT = Datatype_Fun
clasohm@0
    10
 (val thy = Univ.thy;
clasohm@0
    11
  val rec_specs = 
clasohm@0
    12
      [("bt", "univ(A)",
clasohm@0
    13
	  [(["Lf"],"i"), (["Br"],"[i,i,i]=>i")])];
clasohm@0
    14
  val rec_styp = "i=>i";
clasohm@0
    15
  val ext = None
clasohm@0
    16
  val sintrs = 
clasohm@0
    17
	  ["Lf : bt(A)",
clasohm@0
    18
	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
clasohm@0
    19
  val monos = [];
lcp@71
    20
  val type_intrs = datatype_intrs
clasohm@0
    21
  val type_elims = []);
clasohm@0
    22
clasohm@0
    23
val [LfI, BrI] = BT.intrs;
clasohm@0
    24
clasohm@0
    25
(*Perform induction on l, then prove the major premise using prems. *)
clasohm@0
    26
fun bt_ind_tac a prems i = 
clasohm@0
    27
    EVERY [res_inst_tac [("x",a)] BT.induct i,
clasohm@0
    28
	   rename_last_tac a ["1","2"] (i+2),
clasohm@0
    29
	   ares_tac prems i];
clasohm@0
    30
clasohm@0
    31
clasohm@0
    32
(**  Lemmas to justify using "bt" in other recursive type definitions **)
clasohm@0
    33
clasohm@0
    34
goalw BT.thy BT.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
clasohm@0
    35
by (rtac lfp_mono 1);
clasohm@0
    36
by (REPEAT (rtac BT.bnd_mono 1));
clasohm@0
    37
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
clasohm@0
    38
val bt_mono = result();
clasohm@0
    39
clasohm@0
    40
goalw BT.thy (BT.defs@BT.con_defs) "bt(univ(A)) <= univ(A)";
clasohm@0
    41
by (rtac lfp_lowerbound 1);
clasohm@0
    42
by (rtac (A_subset_univ RS univ_mono) 2);
clasohm@0
    43
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
clasohm@0
    44
			    Pair_in_univ]) 1);
clasohm@0
    45
val bt_univ = result();
clasohm@0
    46
lcp@56
    47
val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
clasohm@0
    48