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