src/ZF/ex/BT_Fn.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
permissions -rw-r--r--
Initial revision
     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 (*Used to verify bt_rec*)
    16 val bt_rec_ss = ZF_ss 
    17       addcongs (mk_typed_congs BT_Fn.thy [("h", "[i,i,i,i,i]=>i")])
    18       addrews BT.case_eqns;
    19 
    20 goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))";
    21 by (SIMP_TAC rank_ss 1);
    22 val rank_Br1 = result();
    23 
    24 goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))";
    25 by (SIMP_TAC rank_ss 1);
    26 val rank_Br2 = result();
    27 
    28 goal BT_Fn.thy "bt_rec(Lf,c,h) = c";
    29 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    30 by (SIMP_TAC bt_rec_ss 1);
    31 val bt_rec_Lf = result();
    32 
    33 goal BT_Fn.thy
    34     "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
    35 by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    36 by (SIMP_TAC (bt_rec_ss addrews [Vset_rankI, rank_Br1, rank_Br2]) 1);
    37 val bt_rec_Br = result();
    38 
    39 (*Type checking -- proved by induction, as usual*)
    40 val prems = goal BT_Fn.thy
    41     "[| t: bt(A);    \
    42 \       c: C(Lf);       \
    43 \       !!x y z r s. [| x:A;  y:bt(A);  z:bt(A);  r:C(y);  s:C(z) |] ==> \
    44 \		     h(x,y,z,r,s): C(Br(x,y,z))  \
    45 \    |] ==> bt_rec(t,c,h) : C(t)";
    46 by (bt_ind_tac "t" prems 1);
    47 by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
    48 			    (prems@[bt_rec_Lf,bt_rec_Br]))));
    49 val bt_rec_type = result();
    50 
    51 (** Versions for use with definitions **)
    52 
    53 val [rew] = goal BT_Fn.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
    54 by (rewtac rew);
    55 by (rtac bt_rec_Lf 1);
    56 val def_bt_rec_Lf = result();
    57 
    58 val [rew] = goal BT_Fn.thy
    59     "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
    60 by (rewtac rew);
    61 by (rtac bt_rec_Br 1);
    62 val def_bt_rec_Br = result();
    63 
    64 fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
    65 
    66 (** n_nodes **)
    67 
    68 val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
    69 
    70 val prems = goalw BT_Fn.thy [n_nodes_def] 
    71     "xs: bt(A) ==> n_nodes(xs) : nat";
    72 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
    73 val n_nodes_type = result();
    74 
    75 
    76 (** n_leaves **)
    77 
    78 val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
    79 
    80 val prems = goalw BT_Fn.thy [n_leaves_def] 
    81     "xs: bt(A) ==> n_leaves(xs) : nat";
    82 by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
    83 val n_leaves_type = result();
    84 
    85 (** bt_reflect **)
    86 
    87 val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
    88 
    89 val prems = goalw BT_Fn.thy [bt_reflect_def] 
    90     "xs: bt(A) ==> bt_reflect(xs) : bt(A)";
    91 by (REPEAT (ares_tac (prems @ [bt_rec_type, LfI, BrI]) 1));
    92 val bt_reflect_type = result();
    93 
    94 
    95 (** BT_Fn simplification **)
    96 
    97 
    98 val bt_typechecks =
    99       [LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
   100 
   101 val bt_congs = 
   102     BT.congs @
   103     mk_congs BT_Fn.thy ["bt_case","bt_rec","n_nodes","n_leaves","bt_reflect"];
   104 
   105 val bt_ss = arith_ss 
   106     addcongs bt_congs
   107     addrews BT.case_eqns
   108     addrews bt_typechecks
   109     addrews [bt_rec_Lf, bt_rec_Br, 
   110 	     n_nodes_Lf, n_nodes_Br,
   111 	     n_leaves_Lf, n_leaves_Br,
   112 	     bt_reflect_Lf, bt_reflect_Br];
   113 
   114 
   115 (*** theorems about n_leaves ***)
   116 
   117 val prems = goal BT_Fn.thy
   118     "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
   119 by (bt_ind_tac "t" prems 1);
   120 by (ALLGOALS (ASM_SIMP_TAC bt_ss));
   121 by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
   122 val n_leaves_reflect = result();
   123 
   124 val prems = goal BT_Fn.thy
   125     "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
   126 by (bt_ind_tac "t" prems 1);
   127 by (ALLGOALS (ASM_SIMP_TAC (bt_ss addrews [add_succ_right])));
   128 val n_leaves_nodes = result();
   129 
   130 (*** theorems about bt_reflect ***)
   131 
   132 val prems = goal BT_Fn.thy
   133     "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
   134 by (bt_ind_tac "t" prems 1);
   135 by (ALLGOALS (ASM_SIMP_TAC bt_ss));
   136 val bt_reflect_bt_reflect_ident = result();
   137 
   138