src/ZF/ex/TF.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 529 f0d16216e394
child 739 786f32e0b64e
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
clasohm@0
     1
(*  Title: 	ZF/ex/tf.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Trees & forests, a mutually recursive type definition.
lcp@515
     7
lcp@515
     8
Still needs
lcp@515
     9
lcp@515
    10
"TF_reflect == (%z. TF_rec(z, %x ts r. Tcons(x,r), 0, 
lcp@515
    11
               %t ts r1 r2. TF_of_list(list_of_TF(r2) @ <r1,0>)))"
clasohm@0
    12
*)
clasohm@0
    13
lcp@515
    14
open TF;
clasohm@0
    15
lcp@515
    16
val [TconsI, FnilI, FconsI] = tree_forest.intrs;
clasohm@0
    17
clasohm@0
    18
(** tree_forest(A) as the union of tree(A) and forest(A) **)
clasohm@0
    19
lcp@515
    20
goalw TF.thy (tl tree_forest.defs) "tree(A) <= tree_forest(A)";
clasohm@0
    21
by (rtac Part_subset 1);
clasohm@0
    22
val tree_subset_TF = result();
clasohm@0
    23
lcp@515
    24
goalw TF.thy (tl tree_forest.defs) "forest(A) <= tree_forest(A)";
clasohm@0
    25
by (rtac Part_subset 1);
clasohm@0
    26
val forest_subset_TF = result();
clasohm@0
    27
lcp@515
    28
goalw TF.thy (tl tree_forest.defs) "tree(A) Un forest(A) = tree_forest(A)";
lcp@515
    29
by (rtac (tree_forest.dom_subset RS Part_sum_equality) 1);
clasohm@0
    30
val TF_equals_Un = result();
clasohm@0
    31
clasohm@0
    32
(** NOT useful, but interesting... **)
clasohm@0
    33
lcp@529
    34
goalw TF.thy (tl tree_forest.defs) 
lcp@434
    35
    "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
lcp@529
    36
let open tree_forest;  
lcp@529
    37
    val rew = rewrite_rule (con_defs @ tl defs) in  
lcp@529
    38
by (fast_tac (sum_cs addSIs (equalityI :: PartI :: (map rew intrs RL [PartD1]))
lcp@529
    39
                     addEs [PartE, rew elim]) 1)
lcp@529
    40
end;
lcp@434
    41
val tree_forest_unfold = result();
lcp@434
    42
lcp@529
    43
val tree_forest_unfold' = rewrite_rule (tl tree_forest.defs) 
lcp@529
    44
                          tree_forest_unfold;
lcp@434
    45
lcp@515
    46
goalw TF.thy (tl tree_forest.defs)
lcp@515
    47
    "tree(A) = {Inl(x). x: A*forest(A)}";
lcp@438
    48
by (rtac (Part_Inl RS subst) 1);
lcp@438
    49
by (rtac (tree_forest_unfold' RS subst_context) 1);
clasohm@0
    50
val tree_unfold = result();
clasohm@0
    51
lcp@515
    52
goalw TF.thy (tl tree_forest.defs)
lcp@515
    53
    "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
lcp@438
    54
by (rtac (Part_Inr RS subst) 1);
lcp@438
    55
by (rtac (tree_forest_unfold' RS subst_context) 1);
clasohm@0
    56
val forest_unfold = result();
clasohm@0
    57
lcp@434
    58
lcp@515
    59
(*** TF_rec -- by Vset recursion ***)
lcp@434
    60
lcp@515
    61
(** conversion rules **)
lcp@515
    62
lcp@515
    63
goal TF.thy "TF_rec(Tcons(a,f), b, c, d) = b(a, f, TF_rec(f,b,c,d))";
lcp@515
    64
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
lcp@515
    65
by (rewrite_goals_tac tree_forest.con_defs);
lcp@515
    66
by (simp_tac rank_ss 1);
lcp@515
    67
val TF_rec_Tcons = result();
lcp@515
    68
lcp@515
    69
goal TF.thy "TF_rec(Fnil, b, c, d) = c";
lcp@515
    70
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
lcp@515
    71
by (rewrite_goals_tac tree_forest.con_defs);
lcp@515
    72
by (simp_tac rank_ss 1);
lcp@515
    73
val TF_rec_Fnil = result();
lcp@515
    74
lcp@515
    75
goal TF.thy "TF_rec(Fcons(t,f), b, c, d) = \
lcp@515
    76
\      d(t, f, TF_rec(t, b, c, d), TF_rec(f, b, c, d))";
lcp@515
    77
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
lcp@515
    78
by (rewrite_goals_tac tree_forest.con_defs);
lcp@515
    79
by (simp_tac rank_ss 1);
lcp@515
    80
val TF_rec_Fcons = result();
lcp@515
    81
lcp@515
    82
(*list_ss includes list operations as well as arith_ss*)
lcp@515
    83
val TF_rec_ss = list_ss addsimps
lcp@515
    84
  [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
lcp@515
    85
lcp@515
    86
(** Type checking **)
lcp@515
    87
lcp@515
    88
val major::prems = goal TF.thy
lcp@515
    89
    "[| z: tree_forest(A);  \
lcp@515
    90
\       !!x f r. [| x: A;  f: forest(A);  r: C(f) 		\
lcp@515
    91
\                 |] ==> b(x,f,r): C(Tcons(x,f));     	\
lcp@515
    92
\	c : C(Fnil);        					\
lcp@515
    93
\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: C(f) \
lcp@515
    94
\                     |] ==> d(t,f,r1,r2): C(Fcons(t,f))    	\
lcp@515
    95
\    |] ==> TF_rec(z,b,c,d) : C(z)";
lcp@515
    96
by (rtac (major RS tree_forest.induct) 1);
lcp@515
    97
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
lcp@515
    98
val TF_rec_type = result();
lcp@515
    99
lcp@515
   100
(*Mutually recursive version*)
lcp@515
   101
val prems = goal TF.thy
lcp@515
   102
    "[| !!x f r. [| x: A;  f: forest(A);  r: D(f) 		\
lcp@515
   103
\                 |] ==> b(x,f,r): C(Tcons(x,f));    	 	\
lcp@515
   104
\	c : D(Fnil);        					\
lcp@515
   105
\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: D(f) \
lcp@515
   106
\                     |] ==> d(t,f,r1,r2): D(Fcons(t,f))    	\
lcp@515
   107
\    |] ==> (ALL t:tree(A).    TF_rec(t,b,c,d)  : C(t)) &  	\
lcp@515
   108
\           (ALL f: forest(A). TF_rec(f,b,c,d) : D(f))";
lcp@515
   109
by (rewtac Ball_def);
lcp@515
   110
by (rtac tree_forest.mutual_induct 1);
lcp@515
   111
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
lcp@515
   112
val tree_forest_rec_type = result();
lcp@515
   113
lcp@515
   114
lcp@515
   115
(** Versions for use with definitions **)
lcp@515
   116
lcp@515
   117
val [rew] = goal TF.thy
lcp@515
   118
    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))";
lcp@515
   119
by (rewtac rew);
lcp@515
   120
by (rtac TF_rec_Tcons 1);
lcp@515
   121
val def_TF_rec_Tcons = result();
lcp@515
   122
lcp@515
   123
val [rew] = goal TF.thy
lcp@515
   124
    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
lcp@515
   125
by (rewtac rew);
lcp@515
   126
by (rtac TF_rec_Fnil 1);
lcp@515
   127
val def_TF_rec_Fnil = result();
lcp@515
   128
lcp@515
   129
val [rew] = goal TF.thy
lcp@515
   130
    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))";
lcp@515
   131
by (rewtac rew);
lcp@515
   132
by (rtac TF_rec_Fcons 1);
lcp@515
   133
val def_TF_rec_Fcons = result();
lcp@515
   134
lcp@515
   135
fun TF_recs def = map standard 
lcp@515
   136
    	([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
lcp@515
   137
lcp@515
   138
lcp@515
   139
(** list_of_TF and TF_of_list **)
lcp@515
   140
lcp@515
   141
val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] =
lcp@515
   142
	TF_recs list_of_TF_def;
lcp@515
   143
lcp@515
   144
goalw TF.thy [list_of_TF_def]
lcp@515
   145
    "!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
lcp@515
   146
by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
lcp@515
   147
val list_of_TF_type = result();
lcp@515
   148
lcp@515
   149
val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
lcp@515
   150
lcp@515
   151
goalw TF.thy [TF_of_list_def] 
lcp@515
   152
    "!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
lcp@515
   153
by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
lcp@515
   154
val TF_of_list_type = result();
lcp@515
   155
lcp@515
   156
lcp@515
   157
(** TF_map **)
lcp@515
   158
lcp@515
   159
val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def;
lcp@515
   160
lcp@515
   161
val prems = goalw TF.thy [TF_map_def]
lcp@515
   162
    "[| !!x. x: A ==> h(x): B |] ==> \
lcp@515
   163
\      (ALL t:tree(A). TF_map(h,t) : tree(B)) &  \
lcp@515
   164
\      (ALL f: forest(A). TF_map(h,f) : forest(B))";
lcp@515
   165
by (REPEAT
lcp@515
   166
    (ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
lcp@515
   167
val TF_map_type = result();
lcp@515
   168
lcp@515
   169
lcp@515
   170
(** TF_size **)
lcp@515
   171
lcp@515
   172
val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def;
lcp@515
   173
lcp@515
   174
goalw TF.thy [TF_size_def]
lcp@515
   175
    "!!z A. z: tree_forest(A) ==> TF_size(z) : nat";
lcp@515
   176
by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
lcp@515
   177
val TF_size_type = result();
lcp@515
   178
lcp@515
   179
lcp@515
   180
(** TF_preorder **)
lcp@515
   181
lcp@515
   182
val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] =
lcp@515
   183
	TF_recs TF_preorder_def;
lcp@515
   184
lcp@515
   185
goalw TF.thy [TF_preorder_def]
lcp@515
   186
    "!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)";
lcp@515
   187
by (REPEAT (ares_tac ([TF_rec_type, app_type] @ list.intrs) 1));
lcp@515
   188
val TF_preorder_type = result();
lcp@515
   189
lcp@515
   190
lcp@515
   191
(** Term simplification **)
lcp@515
   192
lcp@515
   193
val treeI = tree_subset_TF RS subsetD
lcp@515
   194
and forestI = forest_subset_TF RS subsetD;
lcp@515
   195
lcp@515
   196
val TF_typechecks =
lcp@515
   197
    [TconsI, FnilI, FconsI, treeI, forestI,
lcp@515
   198
     list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
lcp@515
   199
lcp@515
   200
val TF_rewrites =
lcp@515
   201
   [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
lcp@515
   202
    list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
lcp@515
   203
    TF_of_list_Nil,TF_of_list_Cons,
lcp@515
   204
    TF_map_Tcons, TF_map_Fnil, TF_map_Fcons,
lcp@515
   205
    TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
lcp@515
   206
    TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
lcp@515
   207
lcp@515
   208
val TF_ss = list_ss addsimps TF_rewrites
lcp@515
   209
                    setsolver type_auto_tac (list_typechecks@TF_typechecks);
lcp@515
   210
lcp@515
   211
(** theorems about list_of_TF and TF_of_list **)
lcp@515
   212
lcp@515
   213
(*essentially the same as list induction*)
lcp@515
   214
val major::prems = goal TF.thy 
lcp@515
   215
    "[| f: forest(A);  	\
lcp@515
   216
\       R(Fnil);        \
lcp@515
   217
\       !!t f. [| t: tree(A);  f: forest(A);  R(f) |] ==> R(Fcons(t,f))  \
lcp@515
   218
\    |] ==> R(f)";
lcp@515
   219
by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
lcp@515
   220
by (REPEAT (ares_tac (TrueI::prems) 1));
lcp@515
   221
val forest_induct = result();
lcp@515
   222
lcp@515
   223
goal TF.thy "!!f A. f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
lcp@515
   224
by (etac forest_induct 1);
lcp@515
   225
by (ALLGOALS (asm_simp_tac TF_ss));
lcp@515
   226
val forest_iso = result();
lcp@515
   227
lcp@515
   228
goal TF.thy
lcp@515
   229
    "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
lcp@515
   230
by (etac list.induct 1);
lcp@515
   231
by (ALLGOALS (asm_simp_tac TF_ss));
lcp@515
   232
val tree_list_iso = result();
lcp@515
   233
lcp@515
   234
(** theorems about TF_map **)
lcp@515
   235
lcp@515
   236
goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
lcp@515
   237
by (etac tree_forest.induct 1);
lcp@515
   238
by (ALLGOALS (asm_simp_tac TF_ss));
lcp@515
   239
val TF_map_ident = result();
lcp@515
   240
lcp@515
   241
goal TF.thy
lcp@515
   242
 "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
lcp@515
   243
by (etac tree_forest.induct 1);
lcp@515
   244
by (ALLGOALS (asm_simp_tac TF_ss));
lcp@515
   245
val TF_map_compose = result();
lcp@515
   246
lcp@515
   247
(** theorems about TF_size **)
lcp@515
   248
lcp@515
   249
goal TF.thy
lcp@515
   250
    "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
lcp@515
   251
by (etac tree_forest.induct 1);
lcp@515
   252
by (ALLGOALS (asm_simp_tac TF_ss));
lcp@515
   253
val TF_size_TF_map = result();
lcp@515
   254
lcp@515
   255
goal TF.thy
lcp@515
   256
    "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
lcp@515
   257
by (etac tree_forest.induct 1);
lcp@515
   258
by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
lcp@515
   259
val TF_size_length = result();
lcp@515
   260
lcp@515
   261
(** theorems about TF_preorder **)
lcp@515
   262
lcp@515
   263
goal TF.thy "!!z A. z: tree_forest(A) ==> \
lcp@515
   264
\                      TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
lcp@515
   265
by (etac tree_forest.induct 1);
lcp@515
   266
by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
lcp@515
   267
val TF_preorder_TF_map = result();