src/ZF/ex/TF_Fn.ML
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/TF_Fn.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,233 @@
     1.4 +(*  Title: 	ZF/ex/tf.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For tf.thy.  Trees & forests, a mutually recursive type definition.
    1.10 +
    1.11 +Still needs
    1.12 +
    1.13 +"TF_reflect == (%z. TF_rec(z, %x ts r. Tcons(x,r), 0, 
    1.14 +               %t ts r1 r2. TF_of_list(list_of_TF(r2) @ <r1,0>)))"
    1.15 +*)
    1.16 +
    1.17 +open TF_Fn;
    1.18 +
    1.19 +
    1.20 +(*** TF_rec -- by Vset recursion ***)
    1.21 +
    1.22 +(*Used only to verify TF_rec*)
    1.23 +val TF_congs = mk_typed_congs TF.thy 
    1.24 +		   [("b", "[i,i,i]=>i"), ("d", "[i,i,i,i]=>i")];
    1.25 +
    1.26 +(** conversion rules **)
    1.27 +
    1.28 +goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
    1.29 +by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
    1.30 +by (rewrite_goals_tac TF.con_defs);
    1.31 +by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
    1.32 +val TF_rec_Tcons = result();
    1.33 +
    1.34 +goal TF_Fn.thy "TF_rec(Fnil, b, c, d) = c";
    1.35 +by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
    1.36 +by (rewrite_goals_tac TF.con_defs);
    1.37 +by (SIMP_TAC rank_ss 1);
    1.38 +val TF_rec_Fnil = result();
    1.39 +
    1.40 +goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
    1.41 +\      d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
    1.42 +by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
    1.43 +by (rewrite_goals_tac TF.con_defs);
    1.44 +by (SIMP_TAC (rank_ss addcongs TF_congs) 1);
    1.45 +val TF_rec_Fcons = result();
    1.46 +
    1.47 +(*list_ss includes list operations as well as arith_ss*)
    1.48 +val TF_rec_ss = list_ss addrews
    1.49 +  [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
    1.50 +
    1.51 +(** Type checking **)
    1.52 +
    1.53 +val major::prems = goal TF_Fn.thy
    1.54 +    "[| z: tree_forest(A);  \
    1.55 +\       !!x tf r. [| x: A;  tf: forest(A);  r: C(tf) 		\
    1.56 +\                 |] ==> b(x,tf,r): C(Tcons(x,tf));     	\
    1.57 +\	c : C(Fnil);        					\
    1.58 +\       !!t tf r1 r2. [| t: tree(A);  tf: forest(A);  r1: C(t); r2: C(tf) \
    1.59 +\                     |] ==> d(t,tf,r1,r2): C(Fcons(t,tf))    	\
    1.60 +\    |] ==> TF_rec(z,b,c,d) : C(z)";
    1.61 +by (rtac (major RS TF.induct) 1);
    1.62 +by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
    1.63 +val TF_rec_type = result();
    1.64 +
    1.65 +(*Mutually recursive version*)
    1.66 +val prems = goal TF_Fn.thy
    1.67 +    "[| !!x tf r. [| x: A;  tf: forest(A);  r: D(tf) 		\
    1.68 +\                 |] ==> b(x,tf,r): C(Tcons(x,tf));     	\
    1.69 +\	c : D(Fnil);        					\
    1.70 +\       !!t tf r1 r2. [| t: tree(A);  tf: forest(A);  r1: C(t); r2: D(tf) \
    1.71 +\                     |] ==> d(t,tf,r1,r2): D(Fcons(t,tf))    	\
    1.72 +\    |] ==> (ALL t:tree(A).    TF_rec(t,b,c,d)  : C(t)) &  	\
    1.73 +\           (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
    1.74 +by (rewtac Ball_def);
    1.75 +by (rtac TF.mutual_induct 1);
    1.76 +by (ALLGOALS (ASM_SIMP_TAC (TF_rec_ss addrews prems)));
    1.77 +val tree_forest_rec_type = result();
    1.78 +
    1.79 +
    1.80 +(** Versions for use with definitions **)
    1.81 +
    1.82 +val [rew] = goal TF_Fn.thy
    1.83 +    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,tf)) = b(a,tf,j(tf))";
    1.84 +by (rewtac rew);
    1.85 +by (rtac TF_rec_Tcons 1);
    1.86 +val def_TF_rec_Tcons = result();
    1.87 +
    1.88 +val [rew] = goal TF_Fn.thy
    1.89 +    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
    1.90 +by (rewtac rew);
    1.91 +by (rtac TF_rec_Fnil 1);
    1.92 +val def_TF_rec_Fnil = result();
    1.93 +
    1.94 +val [rew] = goal TF_Fn.thy
    1.95 +    "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,tf)) = d(t,tf,j(t),j(tf))";
    1.96 +by (rewtac rew);
    1.97 +by (rtac TF_rec_Fcons 1);
    1.98 +val def_TF_rec_Fcons = result();
    1.99 +
   1.100 +fun TF_recs def = map standard 
   1.101 +    	([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
   1.102 +
   1.103 +
   1.104 +(** list_of_TF and TF_of_list **)
   1.105 +
   1.106 +val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] =
   1.107 +	TF_recs list_of_TF_def;
   1.108 +
   1.109 +goalw TF_Fn.thy [list_of_TF_def]
   1.110 +    "!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
   1.111 +by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
   1.112 +val list_of_TF_type = result();
   1.113 +
   1.114 +val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
   1.115 +
   1.116 +goalw TF_Fn.thy [TF_of_list_def] 
   1.117 +    "!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
   1.118 +by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
   1.119 +val TF_of_list_type = result();
   1.120 +
   1.121 +
   1.122 +(** TF_map **)
   1.123 +
   1.124 +val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def;
   1.125 +
   1.126 +val prems = goalw TF_Fn.thy [TF_map_def]
   1.127 +    "[| !!x. x: A ==> h(x): B |] ==> \
   1.128 +\      (ALL t:tree(A). TF_map(h,t) : tree(B)) &  \
   1.129 +\      (ALL tf: forest(A). TF_map(h,tf) : forest(B))";
   1.130 +by (REPEAT
   1.131 +    (ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
   1.132 +val TF_map_type = result();
   1.133 +
   1.134 +
   1.135 +(** TF_size **)
   1.136 +
   1.137 +val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def;
   1.138 +
   1.139 +goalw TF_Fn.thy [TF_size_def]
   1.140 +    "!!z A. z: tree_forest(A) ==> TF_size(z) : nat";
   1.141 +by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
   1.142 +val TF_size_type = result();
   1.143 +
   1.144 +
   1.145 +(** TF_preorder **)
   1.146 +
   1.147 +val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] =
   1.148 +	TF_recs TF_preorder_def;
   1.149 +
   1.150 +goalw TF_Fn.thy [TF_preorder_def]
   1.151 +    "!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)";
   1.152 +by (REPEAT (ares_tac [TF_rec_type, app_type,NilI, ConsI] 1));
   1.153 +val TF_preorder_type = result();
   1.154 +
   1.155 +
   1.156 +(** Term simplification **)
   1.157 +
   1.158 +val treeI = tree_subset_TF RS subsetD
   1.159 +and forestI = forest_subset_TF RS subsetD;
   1.160 +
   1.161 +val TF_typechecks =
   1.162 +    [TconsI, FnilI, FconsI, treeI, forestI,
   1.163 +     list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
   1.164 +
   1.165 +val TF_congs = TF.congs @ 
   1.166 +    mk_congs TF_Fn.thy
   1.167 +    ["TF_rec", "list_of_TF", "TF_of_list", "TF_map", "TF_size", "TF_preorder"];
   1.168 +
   1.169 +val TF_rewrites =
   1.170 +   [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
   1.171 +    list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
   1.172 +    TF_of_list_Nil,TF_of_list_Cons,
   1.173 +    TF_map_Tcons, TF_map_Fnil, TF_map_Fcons,
   1.174 +    TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
   1.175 +    TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
   1.176 +
   1.177 +val TF_ss = list_ss addcongs TF_congs 
   1.178 +		    addrews (TF_rewrites@TF_typechecks);
   1.179 +
   1.180 +(** theorems about list_of_TF and TF_of_list **)
   1.181 +
   1.182 +(*essentially the same as list induction*)
   1.183 +val major::prems = goal TF_Fn.thy 
   1.184 +    "[| tf: forest(A);  \
   1.185 +\       R(Fnil);        \
   1.186 +\       !!t tf. [| t: tree(A);  tf: forest(A);  R(tf) |] ==> R(Fcons(t,tf))  \
   1.187 +\    |] ==> R(tf)";
   1.188 +by (rtac (major RS (TF.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
   1.189 +by (REPEAT (ares_tac (TrueI::prems) 1));
   1.190 +val forest_induct = result();
   1.191 +
   1.192 +goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
   1.193 +by (etac forest_induct 1);
   1.194 +by (ALLGOALS (ASM_SIMP_TAC TF_ss));
   1.195 +val forest_iso = result();
   1.196 +
   1.197 +goal TF_Fn.thy
   1.198 +    "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
   1.199 +by (etac List.induct 1);
   1.200 +by (ALLGOALS (ASM_SIMP_TAC TF_ss));
   1.201 +val tree_list_iso = result();
   1.202 +
   1.203 +(** theorems about TF_map **)
   1.204 +
   1.205 +goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
   1.206 +by (etac TF.induct 1);
   1.207 +by (ALLGOALS (ASM_SIMP_TAC TF_ss));
   1.208 +val TF_map_ident = result();
   1.209 +
   1.210 +goal TF_Fn.thy
   1.211 + "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
   1.212 +by (etac TF.induct 1);
   1.213 +by (ALLGOALS (ASM_SIMP_TAC TF_ss));
   1.214 +val TF_map_compose = result();
   1.215 +
   1.216 +(** theorems about TF_size **)
   1.217 +
   1.218 +goal TF_Fn.thy
   1.219 +    "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
   1.220 +by (etac TF.induct 1);
   1.221 +by (ALLGOALS (ASM_SIMP_TAC TF_ss));
   1.222 +val TF_size_TF_map = result();
   1.223 +
   1.224 +goal TF_Fn.thy
   1.225 +    "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
   1.226 +by (etac TF.induct 1);
   1.227 +by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [length_app])));
   1.228 +val TF_size_length = result();
   1.229 +
   1.230 +(** theorems about TF_preorder **)
   1.231 +
   1.232 +goal TF_Fn.thy "!!z A. z: tree_forest(A) ==> \
   1.233 +\                      TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
   1.234 +by (etac TF.induct 1);
   1.235 +by (ALLGOALS (ASM_SIMP_TAC (TF_ss addrews [map_app_distrib])));
   1.236 +val TF_preorder_TF_map = result();