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