src/ZF/ex/TF_Fn.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 77 c94c8ebc0b15
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   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For tf.thy.  Trees & forests, a mutually recursive type definition.
clasohm@0
     7
clasohm@0
     8
Still needs
clasohm@0
     9
clasohm@0
    10
"TF_reflect == (%z. TF_rec(z, %x ts r. Tcons(x,r), 0, 
clasohm@0
    11
               %t ts r1 r2. TF_of_list(list_of_TF(r2) @ <r1,0>)))"
clasohm@0
    12
*)
clasohm@0
    13
clasohm@0
    14
open TF_Fn;
clasohm@0
    15
clasohm@0
    16
clasohm@0
    17
(*** TF_rec -- by Vset recursion ***)
clasohm@0
    18
clasohm@0
    19
(** conversion rules **)
clasohm@0
    20
lcp@77
    21
goal TF_Fn.thy "TF_rec(Tcons(a,f), b, c, d) = b(a, f, TF_rec(f,b,c,d))";
clasohm@0
    22
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
clasohm@0
    23
by (rewrite_goals_tac TF.con_defs);
lcp@7
    24
by (simp_tac rank_ss 1);
clasohm@0
    25
val TF_rec_Tcons = result();
clasohm@0
    26
clasohm@0
    27
goal TF_Fn.thy "TF_rec(Fnil, b, c, d) = c";
clasohm@0
    28
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
clasohm@0
    29
by (rewrite_goals_tac TF.con_defs);
lcp@7
    30
by (simp_tac rank_ss 1);
clasohm@0
    31
val TF_rec_Fnil = result();
clasohm@0
    32
lcp@77
    33
goal TF_Fn.thy "TF_rec(Fcons(t,f), b, c, d) = \
lcp@77
    34
\      d(t, f, TF_rec(t, b, c, d), TF_rec(f, b, c, d))";
clasohm@0
    35
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
clasohm@0
    36
by (rewrite_goals_tac TF.con_defs);
lcp@7
    37
by (simp_tac rank_ss 1);
clasohm@0
    38
val TF_rec_Fcons = result();
clasohm@0
    39
clasohm@0
    40
(*list_ss includes list operations as well as arith_ss*)
lcp@7
    41
val TF_rec_ss = list_ss addsimps
clasohm@0
    42
  [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
clasohm@0
    43
clasohm@0
    44
(** Type checking **)
clasohm@0
    45
clasohm@0
    46
val major::prems = goal TF_Fn.thy
clasohm@0
    47
    "[| z: tree_forest(A);  \
lcp@77
    48
\       !!x f r. [| x: A;  f: forest(A);  r: C(f) 		\
lcp@77
    49
\                 |] ==> b(x,f,r): C(Tcons(x,f));     	\
clasohm@0
    50
\	c : C(Fnil);        					\
lcp@77
    51
\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: C(f) \
lcp@77
    52
\                     |] ==> d(t,f,r1,r2): C(Fcons(t,f))    	\
clasohm@0
    53
\    |] ==> TF_rec(z,b,c,d) : C(z)";
clasohm@0
    54
by (rtac (major RS TF.induct) 1);
lcp@7
    55
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
clasohm@0
    56
val TF_rec_type = result();
clasohm@0
    57
clasohm@0
    58
(*Mutually recursive version*)
clasohm@0
    59
val prems = goal TF_Fn.thy
lcp@77
    60
    "[| !!x f r. [| x: A;  f: forest(A);  r: D(f) 		\
lcp@77
    61
\                 |] ==> b(x,f,r): C(Tcons(x,f));    	 	\
clasohm@0
    62
\	c : D(Fnil);        					\
lcp@77
    63
\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: D(f) \
lcp@77
    64
\                     |] ==> d(t,f,r1,r2): D(Fcons(t,f))    	\
clasohm@0
    65
\    |] ==> (ALL t:tree(A).    TF_rec(t,b,c,d)  : C(t)) &  	\
lcp@77
    66
\           (ALL f: forest(A). TF_rec(f,b,c,d) : D(f))";
clasohm@0
    67
by (rewtac Ball_def);
clasohm@0
    68
by (rtac TF.mutual_induct 1);
lcp@7
    69
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
clasohm@0
    70
val tree_forest_rec_type = result();
clasohm@0
    71
clasohm@0
    72
clasohm@0
    73
(** Versions for use with definitions **)
clasohm@0
    74
clasohm@0
    75
val [rew] = goal TF_Fn.thy
lcp@77
    76
    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))";
clasohm@0
    77
by (rewtac rew);
clasohm@0
    78
by (rtac TF_rec_Tcons 1);
clasohm@0
    79
val def_TF_rec_Tcons = result();
clasohm@0
    80
clasohm@0
    81
val [rew] = goal TF_Fn.thy
clasohm@0
    82
    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
clasohm@0
    83
by (rewtac rew);
clasohm@0
    84
by (rtac TF_rec_Fnil 1);
clasohm@0
    85
val def_TF_rec_Fnil = result();
clasohm@0
    86
clasohm@0
    87
val [rew] = goal TF_Fn.thy
lcp@77
    88
    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))";
clasohm@0
    89
by (rewtac rew);
clasohm@0
    90
by (rtac TF_rec_Fcons 1);
clasohm@0
    91
val def_TF_rec_Fcons = result();
clasohm@0
    92
clasohm@0
    93
fun TF_recs def = map standard 
clasohm@0
    94
    	([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
clasohm@0
    95
clasohm@0
    96
clasohm@0
    97
(** list_of_TF and TF_of_list **)
clasohm@0
    98
clasohm@0
    99
val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] =
clasohm@0
   100
	TF_recs list_of_TF_def;
clasohm@0
   101
clasohm@0
   102
goalw TF_Fn.thy [list_of_TF_def]
clasohm@0
   103
    "!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
clasohm@0
   104
by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
clasohm@0
   105
val list_of_TF_type = result();
clasohm@0
   106
clasohm@0
   107
val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
clasohm@0
   108
clasohm@0
   109
goalw TF_Fn.thy [TF_of_list_def] 
clasohm@0
   110
    "!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
clasohm@0
   111
by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
clasohm@0
   112
val TF_of_list_type = result();
clasohm@0
   113
clasohm@0
   114
clasohm@0
   115
(** TF_map **)
clasohm@0
   116
clasohm@0
   117
val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def;
clasohm@0
   118
clasohm@0
   119
val prems = goalw TF_Fn.thy [TF_map_def]
clasohm@0
   120
    "[| !!x. x: A ==> h(x): B |] ==> \
clasohm@0
   121
\      (ALL t:tree(A). TF_map(h,t) : tree(B)) &  \
lcp@77
   122
\      (ALL f: forest(A). TF_map(h,f) : forest(B))";
clasohm@0
   123
by (REPEAT
clasohm@0
   124
    (ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
clasohm@0
   125
val TF_map_type = result();
clasohm@0
   126
clasohm@0
   127
clasohm@0
   128
(** TF_size **)
clasohm@0
   129
clasohm@0
   130
val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def;
clasohm@0
   131
clasohm@0
   132
goalw TF_Fn.thy [TF_size_def]
clasohm@0
   133
    "!!z A. z: tree_forest(A) ==> TF_size(z) : nat";
clasohm@0
   134
by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
clasohm@0
   135
val TF_size_type = result();
clasohm@0
   136
clasohm@0
   137
clasohm@0
   138
(** TF_preorder **)
clasohm@0
   139
clasohm@0
   140
val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] =
clasohm@0
   141
	TF_recs TF_preorder_def;
clasohm@0
   142
clasohm@0
   143
goalw TF_Fn.thy [TF_preorder_def]
clasohm@0
   144
    "!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)";
clasohm@0
   145
by (REPEAT (ares_tac [TF_rec_type, app_type,NilI, ConsI] 1));
clasohm@0
   146
val TF_preorder_type = result();
clasohm@0
   147
clasohm@0
   148
clasohm@0
   149
(** Term simplification **)
clasohm@0
   150
clasohm@0
   151
val treeI = tree_subset_TF RS subsetD
clasohm@0
   152
and forestI = forest_subset_TF RS subsetD;
clasohm@0
   153
clasohm@0
   154
val TF_typechecks =
clasohm@0
   155
    [TconsI, FnilI, FconsI, treeI, forestI,
clasohm@0
   156
     list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
clasohm@0
   157
clasohm@0
   158
val TF_rewrites =
clasohm@0
   159
   [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
clasohm@0
   160
    list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
clasohm@0
   161
    TF_of_list_Nil,TF_of_list_Cons,
clasohm@0
   162
    TF_map_Tcons, TF_map_Fnil, TF_map_Fcons,
clasohm@0
   163
    TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
clasohm@0
   164
    TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
clasohm@0
   165
lcp@7
   166
val TF_ss = list_ss addsimps TF_rewrites
lcp@7
   167
                    setsolver type_auto_tac (list_typechecks@TF_typechecks);
clasohm@0
   168
clasohm@0
   169
(** theorems about list_of_TF and TF_of_list **)
clasohm@0
   170
clasohm@0
   171
(*essentially the same as list induction*)
clasohm@0
   172
val major::prems = goal TF_Fn.thy 
lcp@77
   173
    "[| f: forest(A);  	\
clasohm@0
   174
\       R(Fnil);        \
lcp@77
   175
\       !!t f. [| t: tree(A);  f: forest(A);  R(f) |] ==> R(Fcons(t,f))  \
lcp@77
   176
\    |] ==> R(f)";
clasohm@0
   177
by (rtac (major RS (TF.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
clasohm@0
   178
by (REPEAT (ares_tac (TrueI::prems) 1));
clasohm@0
   179
val forest_induct = result();
clasohm@0
   180
lcp@77
   181
goal TF_Fn.thy "!!f A. f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
clasohm@0
   182
by (etac forest_induct 1);
lcp@7
   183
by (ALLGOALS (asm_simp_tac TF_ss));
clasohm@0
   184
val forest_iso = result();
clasohm@0
   185
clasohm@0
   186
goal TF_Fn.thy
clasohm@0
   187
    "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
clasohm@0
   188
by (etac List.induct 1);
lcp@7
   189
by (ALLGOALS (asm_simp_tac TF_ss));
clasohm@0
   190
val tree_list_iso = result();
clasohm@0
   191
clasohm@0
   192
(** theorems about TF_map **)
clasohm@0
   193
clasohm@0
   194
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
clasohm@0
   195
by (etac TF.induct 1);
lcp@7
   196
by (ALLGOALS (asm_simp_tac TF_ss));
clasohm@0
   197
val TF_map_ident = result();
clasohm@0
   198
clasohm@0
   199
goal TF_Fn.thy
clasohm@0
   200
 "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
clasohm@0
   201
by (etac TF.induct 1);
lcp@7
   202
by (ALLGOALS (asm_simp_tac TF_ss));
clasohm@0
   203
val TF_map_compose = result();
clasohm@0
   204
clasohm@0
   205
(** theorems about TF_size **)
clasohm@0
   206
clasohm@0
   207
goal TF_Fn.thy
clasohm@0
   208
    "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
clasohm@0
   209
by (etac TF.induct 1);
lcp@7
   210
by (ALLGOALS (asm_simp_tac TF_ss));
clasohm@0
   211
val TF_size_TF_map = result();
clasohm@0
   212
clasohm@0
   213
goal TF_Fn.thy
clasohm@0
   214
    "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
clasohm@0
   215
by (etac TF.induct 1);
lcp@7
   216
by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
clasohm@0
   217
val TF_size_length = result();
clasohm@0
   218
clasohm@0
   219
(** theorems about TF_preorder **)
clasohm@0
   220
clasohm@0
   221
goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> \
clasohm@0
   222
\                      TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
clasohm@0
   223
by (etac TF.induct 1);
lcp@7
   224
by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
clasohm@0
   225
val TF_preorder_TF_map = result();