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