src/ZF/ex/BT_Fn.ML
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/BT_Fn.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,138 @@
     1.4 +(*  Title: 	ZF/bt.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For bt.thy.  Binary trees
    1.10 +*)
    1.11 +
    1.12 +open BT_Fn;
    1.13 +
    1.14 +
    1.15 +
    1.16 +(** bt_rec -- by Vset recursion **)
    1.17 +
    1.18 +(*Used to verify bt_rec*)
    1.19 +val bt_rec_ss = ZF_ss 
    1.20 +      addcongs (mk_typed_congs BT_Fn.thy [("h", "[i,i,i,i,i]=>i")])
    1.21 +      addrews BT.case_eqns;
    1.22 +
    1.23 +goalw BT.thy BT.con_defs "rank(l) : rank(Br(a,l,r))";
    1.24 +by (SIMP_TAC rank_ss 1);
    1.25 +val rank_Br1 = result();
    1.26 +
    1.27 +goalw BT.thy BT.con_defs "rank(r) : rank(Br(a,l,r))";
    1.28 +by (SIMP_TAC rank_ss 1);
    1.29 +val rank_Br2 = result();
    1.30 +
    1.31 +goal BT_Fn.thy "bt_rec(Lf,c,h) = c";
    1.32 +by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    1.33 +by (SIMP_TAC bt_rec_ss 1);
    1.34 +val bt_rec_Lf = result();
    1.35 +
    1.36 +goal BT_Fn.thy
    1.37 +    "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
    1.38 +by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
    1.39 +by (SIMP_TAC (bt_rec_ss addrews [Vset_rankI, rank_Br1, rank_Br2]) 1);
    1.40 +val bt_rec_Br = result();
    1.41 +
    1.42 +(*Type checking -- proved by induction, as usual*)
    1.43 +val prems = goal BT_Fn.thy
    1.44 +    "[| t: bt(A);    \
    1.45 +\       c: C(Lf);       \
    1.46 +\       !!x y z r s. [| x:A;  y:bt(A);  z:bt(A);  r:C(y);  s:C(z) |] ==> \
    1.47 +\		     h(x,y,z,r,s): C(Br(x,y,z))  \
    1.48 +\    |] ==> bt_rec(t,c,h) : C(t)";
    1.49 +by (bt_ind_tac "t" prems 1);
    1.50 +by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
    1.51 +			    (prems@[bt_rec_Lf,bt_rec_Br]))));
    1.52 +val bt_rec_type = result();
    1.53 +
    1.54 +(** Versions for use with definitions **)
    1.55 +
    1.56 +val [rew] = goal BT_Fn.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
    1.57 +by (rewtac rew);
    1.58 +by (rtac bt_rec_Lf 1);
    1.59 +val def_bt_rec_Lf = result();
    1.60 +
    1.61 +val [rew] = goal BT_Fn.thy
    1.62 +    "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
    1.63 +by (rewtac rew);
    1.64 +by (rtac bt_rec_Br 1);
    1.65 +val def_bt_rec_Br = result();
    1.66 +
    1.67 +fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
    1.68 +
    1.69 +(** n_nodes **)
    1.70 +
    1.71 +val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
    1.72 +
    1.73 +val prems = goalw BT_Fn.thy [n_nodes_def] 
    1.74 +    "xs: bt(A) ==> n_nodes(xs) : nat";
    1.75 +by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
    1.76 +val n_nodes_type = result();
    1.77 +
    1.78 +
    1.79 +(** n_leaves **)
    1.80 +
    1.81 +val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
    1.82 +
    1.83 +val prems = goalw BT_Fn.thy [n_leaves_def] 
    1.84 +    "xs: bt(A) ==> n_leaves(xs) : nat";
    1.85 +by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
    1.86 +val n_leaves_type = result();
    1.87 +
    1.88 +(** bt_reflect **)
    1.89 +
    1.90 +val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
    1.91 +
    1.92 +val prems = goalw BT_Fn.thy [bt_reflect_def] 
    1.93 +    "xs: bt(A) ==> bt_reflect(xs) : bt(A)";
    1.94 +by (REPEAT (ares_tac (prems @ [bt_rec_type, LfI, BrI]) 1));
    1.95 +val bt_reflect_type = result();
    1.96 +
    1.97 +
    1.98 +(** BT_Fn simplification **)
    1.99 +
   1.100 +
   1.101 +val bt_typechecks =
   1.102 +      [LfI, BrI, bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
   1.103 +
   1.104 +val bt_congs = 
   1.105 +    BT.congs @
   1.106 +    mk_congs BT_Fn.thy ["bt_case","bt_rec","n_nodes","n_leaves","bt_reflect"];
   1.107 +
   1.108 +val bt_ss = arith_ss 
   1.109 +    addcongs bt_congs
   1.110 +    addrews BT.case_eqns
   1.111 +    addrews bt_typechecks
   1.112 +    addrews [bt_rec_Lf, bt_rec_Br, 
   1.113 +	     n_nodes_Lf, n_nodes_Br,
   1.114 +	     n_leaves_Lf, n_leaves_Br,
   1.115 +	     bt_reflect_Lf, bt_reflect_Br];
   1.116 +
   1.117 +
   1.118 +(*** theorems about n_leaves ***)
   1.119 +
   1.120 +val prems = goal BT_Fn.thy
   1.121 +    "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
   1.122 +by (bt_ind_tac "t" prems 1);
   1.123 +by (ALLGOALS (ASM_SIMP_TAC bt_ss));
   1.124 +by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
   1.125 +val n_leaves_reflect = result();
   1.126 +
   1.127 +val prems = goal BT_Fn.thy
   1.128 +    "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
   1.129 +by (bt_ind_tac "t" prems 1);
   1.130 +by (ALLGOALS (ASM_SIMP_TAC (bt_ss addrews [add_succ_right])));
   1.131 +val n_leaves_nodes = result();
   1.132 +
   1.133 +(*** theorems about bt_reflect ***)
   1.134 +
   1.135 +val prems = goal BT_Fn.thy
   1.136 +    "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
   1.137 +by (bt_ind_tac "t" prems 1);
   1.138 +by (ALLGOALS (ASM_SIMP_TAC bt_ss));
   1.139 +val bt_reflect_bt_reflect_ident = result();
   1.140 +
   1.141 +