src/ZF/ex/bt_fn.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 29 4ec9b266ccd1
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/bt.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 For bt.thy.  Binary trees
     7 *)
     8 
     9 open BT_Fn;
    10 
    11 
    12 
    13 (** bt_rec -- by Vset recursion **)
    14 
    15 goalw BT.thy BT.con_defs "rank(l) < rank(Br(a,l,r))";
    16 by (simp_tac rank_ss 1);
    17 val rank_Br1 = result();
    18 
    19 goalw BT.thy BT.con_defs "rank(r) < rank(Br(a,l,r))";
    20 by (simp_tac rank_ss 1);
    21 val rank_Br2 = result();
    22 
    23 goal BT_Fn.thy "bt_rec(Lf,c,h) = c";
    24 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    25 by (simp_tac (ZF_ss addsimps BT.case_eqns) 1);
    26 val bt_rec_Lf = result();
    27 
    28 goal BT_Fn.thy
    29     "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
    30 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    31 by (simp_tac (rank_ss addsimps (BT.case_eqns @ [rank_Br1, rank_Br2])) 1);
    32 val bt_rec_Br = result();
    33 
    34 (*Type checking -- proved by induction, as usual*)
    35 val prems = goal BT_Fn.thy
    36     "[| t: bt(A);    \
    37 \       c: C(Lf);       \
    38 \       !!x y z r s. [| x:A;  y:bt(A);  z:bt(A);  r:C(y);  s:C(z) |] ==> \
    39 \		     h(x,y,z,r,s): C(Br(x,y,z))  \
    40 \    |] ==> bt_rec(t,c,h) : C(t)";
    41 by (bt_ind_tac "t" prems 1);
    42 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
    43 			    (prems@[bt_rec_Lf,bt_rec_Br]))));
    44 val bt_rec_type = result();
    45 
    46 (** Versions for use with definitions **)
    47 
    48 val [rew] = goal BT_Fn.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
    49 by (rewtac rew);
    50 by (rtac bt_rec_Lf 1);
    51 val def_bt_rec_Lf = result();
    52 
    53 val [rew] = goal BT_Fn.thy
    54     "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
    55 by (rewtac rew);
    56 by (rtac bt_rec_Br 1);
    57 val def_bt_rec_Br = result();
    58 
    59 fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
    60 
    61 (** n_nodes **)
    62 
    63 val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
    64 
    65 val prems = goalw BT_Fn.thy [n_nodes_def] 
    66     "xs: bt(A) ==> n_nodes(xs) : nat";
    67 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
    68 val n_nodes_type = result();
    69 
    70 
    71 (** n_leaves **)
    72 
    73 val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
    74 
    75 val prems = goalw BT_Fn.thy [n_leaves_def] 
    76     "xs: bt(A) ==> n_leaves(xs) : nat";
    77 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
    78 val n_leaves_type = result();
    79 
    80 (** bt_reflect **)
    81 
    82 val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
    83 
    84 val prems = goalw BT_Fn.thy [bt_reflect_def] 
    85     "xs: bt(A) ==> bt_reflect(xs) : bt(A)";
    86 by (REPEAT (ares_tac (prems @ [bt_rec_type, LfI, BrI]) 1));
    87 val bt_reflect_type = result();
    88 
    89 
    90 (** BT_Fn simplification **)
    91 
    92 
    93 val bt_typechecks =
    94       [LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
    95 
    96 val bt_ss = arith_ss 
    97     addsimps BT.case_eqns
    98     addsimps bt_typechecks
    99     addsimps [bt_rec_Lf, bt_rec_Br, 
   100 	     n_nodes_Lf, n_nodes_Br,
   101 	     n_leaves_Lf, n_leaves_Br,
   102 	     bt_reflect_Lf, bt_reflect_Br];
   103 
   104 
   105 (*** theorems about n_leaves ***)
   106 
   107 val prems = goal BT_Fn.thy
   108     "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
   109 by (bt_ind_tac "t" prems 1);
   110 by (ALLGOALS (asm_simp_tac bt_ss));
   111 by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
   112 val n_leaves_reflect = result();
   113 
   114 val prems = goal BT_Fn.thy
   115     "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
   116 by (bt_ind_tac "t" prems 1);
   117 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
   118 val n_leaves_nodes = result();
   119 
   120 (*** theorems about bt_reflect ***)
   121 
   122 val prems = goal BT_Fn.thy
   123     "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
   124 by (bt_ind_tac "t" prems 1);
   125 by (ALLGOALS (asm_simp_tac bt_ss));
   126 val bt_reflect_bt_reflect_ident = result();
   127 
   128