src/ZF/ex/BT.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 760 f0200e91b272
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   1994  University of Cambridge
     5 
     6 Datatype definition of binary trees
     7 *)
     8 
     9 open BT;
    10 
    11 (*Perform induction on l, then prove the major premise using prems. *)
    12 fun bt_ind_tac a prems i = 
    13     EVERY [res_inst_tac [("x",a)] bt.induct i,
    14 	   rename_last_tac a ["1","2"] (i+2),
    15 	   ares_tac prems i];
    16 
    17 
    18 (**  Lemmas to justify using "bt" in other recursive type definitions **)
    19 
    20 goalw BT.thy bt.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
    21 by (rtac lfp_mono 1);
    22 by (REPEAT (rtac bt.bnd_mono 1));
    23 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
    24 val bt_mono = result();
    25 
    26 goalw BT.thy (bt.defs@bt.con_defs) "bt(univ(A)) <= univ(A)";
    27 by (rtac lfp_lowerbound 1);
    28 by (rtac (A_subset_univ RS univ_mono) 2);
    29 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
    30 			    Pair_in_univ]) 1);
    31 val bt_univ = result();
    32 
    33 val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
    34 
    35 
    36 (** bt_rec -- by Vset recursion **)
    37 
    38 goalw BT.thy bt.con_defs "rank(l) < rank(Br(a,l,r))";
    39 by (simp_tac rank_ss 1);
    40 val rank_Br1 = result();
    41 
    42 goalw BT.thy bt.con_defs "rank(r) < rank(Br(a,l,r))";
    43 by (simp_tac rank_ss 1);
    44 val rank_Br2 = result();
    45 
    46 goal BT.thy "bt_rec(Lf,c,h) = c";
    47 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    48 by (simp_tac (ZF_ss addsimps bt.case_eqns) 1);
    49 val bt_rec_Lf = result();
    50 
    51 goal BT.thy
    52     "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
    53 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    54 by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1);
    55 val bt_rec_Br = result();
    56 
    57 (*Type checking -- proved by induction, as usual*)
    58 val prems = goal BT.thy
    59     "[| t: bt(A);    \
    60 \       c: C(Lf);       \
    61 \       !!x y z r s. [| x:A;  y:bt(A);  z:bt(A);  r:C(y);  s:C(z) |] ==> \
    62 \		     h(x,y,z,r,s): C(Br(x,y,z))  \
    63 \    |] ==> bt_rec(t,c,h) : C(t)";
    64 by (bt_ind_tac "t" prems 1);
    65 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
    66 			    (prems@[bt_rec_Lf,bt_rec_Br]))));
    67 val bt_rec_type = result();
    68 
    69 (** Versions for use with definitions **)
    70 
    71 val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
    72 by (rewtac rew);
    73 by (rtac bt_rec_Lf 1);
    74 val def_bt_rec_Lf = result();
    75 
    76 val [rew] = goal BT.thy
    77     "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
    78 by (rewtac rew);
    79 by (rtac bt_rec_Br 1);
    80 val def_bt_rec_Br = result();
    81 
    82 fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
    83 
    84 (** n_nodes **)
    85 
    86 val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
    87 
    88 val prems = goalw BT.thy [n_nodes_def] 
    89     "xs: bt(A) ==> n_nodes(xs) : nat";
    90 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
    91 val n_nodes_type = result();
    92 
    93 
    94 (** n_leaves **)
    95 
    96 val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
    97 
    98 val prems = goalw BT.thy [n_leaves_def] 
    99     "xs: bt(A) ==> n_leaves(xs) : nat";
   100 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
   101 val n_leaves_type = result();
   102 
   103 (** bt_reflect **)
   104 
   105 val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
   106 
   107 goalw BT.thy [bt_reflect_def] "!!xs. xs: bt(A) ==> bt_reflect(xs) : bt(A)";
   108 by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
   109 val bt_reflect_type = result();
   110 
   111 
   112 (** BT simplification **)
   113 
   114 
   115 val bt_typechecks =
   116     bt.intrs @ [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
   117 
   118 val bt_ss = arith_ss 
   119     addsimps bt.case_eqns
   120     addsimps bt_typechecks
   121     addsimps [bt_rec_Lf, bt_rec_Br, 
   122 	     n_nodes_Lf, n_nodes_Br,
   123 	     n_leaves_Lf, n_leaves_Br,
   124 	     bt_reflect_Lf, bt_reflect_Br];
   125 
   126 
   127 (*** theorems about n_leaves ***)
   128 
   129 val prems = goal BT.thy
   130     "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
   131 by (bt_ind_tac "t" prems 1);
   132 by (ALLGOALS (asm_simp_tac bt_ss));
   133 by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
   134 val n_leaves_reflect = result();
   135 
   136 val prems = goal BT.thy
   137     "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
   138 by (bt_ind_tac "t" prems 1);
   139 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
   140 val n_leaves_nodes = result();
   141 
   142 (*** theorems about bt_reflect ***)
   143 
   144 val prems = goal BT.thy
   145     "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
   146 by (bt_ind_tac "t" prems 1);
   147 by (ALLGOALS (asm_simp_tac bt_ss));
   148 val bt_reflect_bt_reflect_ident = result();
   149 
   150