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