src/ZF/ListFn.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ListFn.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,306 @@
     1.4 +(*  Title: 	ZF/list-fn.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 list-fn.thy.  Lists in Zermelo-Fraenkel Set Theory 
    1.10 +*)
    1.11 +
    1.12 +open ListFn;
    1.13 +
    1.14 +
    1.15 +(** list_rec -- by Vset recursion **)
    1.16 +
    1.17 +(*Used to verify list_rec*)
    1.18 +val list_rec_ss = ZF_ss 
    1.19 +      addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
    1.20 +      addrews List.case_eqns;
    1.21 +
    1.22 +goal ListFn.thy "list_rec(Nil,c,h) = c";
    1.23 +by (rtac (list_rec_def RS def_Vrec RS trans) 1);
    1.24 +by (SIMP_TAC list_rec_ss 1);
    1.25 +val list_rec_Nil = result();
    1.26 +
    1.27 +goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
    1.28 +by (rtac (list_rec_def RS def_Vrec RS trans) 1);
    1.29 +by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
    1.30 +val list_rec_Cons = result();
    1.31 +
    1.32 +(*Type checking -- proved by induction, as usual*)
    1.33 +val prems = goal ListFn.thy
    1.34 +    "[| l: list(A);    \
    1.35 +\       c: C(Nil);       \
    1.36 +\       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
    1.37 +\    |] ==> list_rec(l,c,h) : C(l)";
    1.38 +by (list_ind_tac "l" prems 1);
    1.39 +by (ALLGOALS (ASM_SIMP_TAC
    1.40 +	      (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
    1.41 +val list_rec_type = result();
    1.42 +
    1.43 +(** Versions for use with definitions **)
    1.44 +
    1.45 +val [rew] = goal ListFn.thy
    1.46 +    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
    1.47 +by (rewtac rew);
    1.48 +by (rtac list_rec_Nil 1);
    1.49 +val def_list_rec_Nil = result();
    1.50 +
    1.51 +val [rew] = goal ListFn.thy
    1.52 +    "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
    1.53 +by (rewtac rew);
    1.54 +by (rtac list_rec_Cons 1);
    1.55 +val def_list_rec_Cons = result();
    1.56 +
    1.57 +fun list_recs def = map standard
    1.58 +    	([def] RL [def_list_rec_Nil, def_list_rec_Cons]);
    1.59 +
    1.60 +(** map **)
    1.61 +
    1.62 +val [map_Nil,map_Cons] = list_recs map_def;
    1.63 +
    1.64 +val prems = goalw ListFn.thy [map_def] 
    1.65 +    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
    1.66 +by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1));
    1.67 +val map_type = result();
    1.68 +
    1.69 +val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
    1.70 +by (rtac (major RS map_type) 1);
    1.71 +by (etac RepFunI 1);
    1.72 +val map_type2 = result();
    1.73 +
    1.74 +(** length **)
    1.75 +
    1.76 +val [length_Nil,length_Cons] = list_recs length_def;
    1.77 +
    1.78 +val prems = goalw ListFn.thy [length_def] 
    1.79 +    "l: list(A) ==> length(l) : nat";
    1.80 +by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1));
    1.81 +val length_type = result();
    1.82 +
    1.83 +(** app **)
    1.84 +
    1.85 +val [app_Nil,app_Cons] = list_recs app_def;
    1.86 +
    1.87 +val prems = goalw ListFn.thy [app_def] 
    1.88 +    "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
    1.89 +by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1));
    1.90 +val app_type = result();
    1.91 +
    1.92 +(** rev **)
    1.93 +
    1.94 +val [rev_Nil,rev_Cons] = list_recs rev_def;
    1.95 +
    1.96 +val prems = goalw ListFn.thy [rev_def] 
    1.97 +    "xs: list(A) ==> rev(xs) : list(A)";
    1.98 +by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
    1.99 +val rev_type = result();
   1.100 +
   1.101 +
   1.102 +(** flat **)
   1.103 +
   1.104 +val [flat_Nil,flat_Cons] = list_recs flat_def;
   1.105 +
   1.106 +val prems = goalw ListFn.thy [flat_def] 
   1.107 +    "ls: list(list(A)) ==> flat(ls) : list(A)";
   1.108 +by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));
   1.109 +val flat_type = result();
   1.110 +
   1.111 +
   1.112 +(** list_add **)
   1.113 +
   1.114 +val [list_add_Nil,list_add_Cons] = list_recs list_add_def;
   1.115 +
   1.116 +val prems = goalw ListFn.thy [list_add_def] 
   1.117 +    "xs: list(nat) ==> list_add(xs) : nat";
   1.118 +by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1));
   1.119 +val list_add_type = result();
   1.120 +
   1.121 +(** ListFn simplification **)
   1.122 +
   1.123 +val list_typechecks =
   1.124 +      [NilI, ConsI, list_rec_type,
   1.125 +       map_type, map_type2, app_type, length_type, rev_type, flat_type,
   1.126 +       list_add_type];
   1.127 +
   1.128 +val list_congs = 
   1.129 +    List.congs @ 
   1.130 +    mk_congs ListFn.thy
   1.131 +        ["list_rec","map","op @","length","rev","flat","list_add"];
   1.132 +
   1.133 +val list_ss = arith_ss 
   1.134 +    addcongs list_congs
   1.135 +    addrews List.case_eqns
   1.136 +    addrews list_typechecks
   1.137 +    addrews [list_rec_Nil, list_rec_Cons, 
   1.138 +	     map_Nil, map_Cons,
   1.139 +	     app_Nil, app_Cons,
   1.140 +	     length_Nil, length_Cons,
   1.141 +	     rev_Nil, rev_Cons,
   1.142 +	     flat_Nil, flat_Cons,
   1.143 +	     list_add_Nil, list_add_Cons];
   1.144 +
   1.145 +(*** theorems about map ***)
   1.146 +
   1.147 +val prems = goal ListFn.thy
   1.148 +    "l: list(A) ==> map(%u.u, l) = l";
   1.149 +by (list_ind_tac "l" prems 1);
   1.150 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.151 +val map_ident = result();
   1.152 +
   1.153 +val prems = goal ListFn.thy
   1.154 +    "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
   1.155 +by (list_ind_tac "l" prems 1);
   1.156 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.157 +val map_compose = result();
   1.158 +
   1.159 +val prems = goal ListFn.thy
   1.160 +    "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
   1.161 +by (list_ind_tac "xs" prems 1);
   1.162 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.163 +val map_app_distrib = result();
   1.164 +
   1.165 +val prems = goal ListFn.thy
   1.166 +    "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
   1.167 +by (list_ind_tac "ls" prems 1);
   1.168 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
   1.169 +val map_flat = result();
   1.170 +
   1.171 +val prems = goal ListFn.thy
   1.172 +    "l: list(A) ==> \
   1.173 +\    list_rec(map(h,l), c, d) = \
   1.174 +\    list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
   1.175 +by (list_ind_tac "l" prems 1);
   1.176 +by (ALLGOALS 
   1.177 +    (ASM_SIMP_TAC 
   1.178 +     (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
   1.179 +val list_rec_map = result();
   1.180 +
   1.181 +(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
   1.182 +
   1.183 +(* c : list(Collect(B,P)) ==> c : list(B) *)
   1.184 +val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);
   1.185 +
   1.186 +val prems = goal ListFn.thy
   1.187 +    "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
   1.188 +by (list_ind_tac "l" prems 1);
   1.189 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.190 +val map_list_Collect = result();
   1.191 +
   1.192 +(*** theorems about length ***)
   1.193 +
   1.194 +val prems = goal ListFn.thy
   1.195 +    "xs: list(A) ==> length(map(h,xs)) = length(xs)";
   1.196 +by (list_ind_tac "xs" prems 1);
   1.197 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.198 +val length_map = result();
   1.199 +
   1.200 +val prems = goal ListFn.thy
   1.201 +    "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
   1.202 +by (list_ind_tac "xs" prems 1);
   1.203 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.204 +val length_app = result();
   1.205 +
   1.206 +(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m 
   1.207 +   Used for rewriting below*)
   1.208 +val add_commute_succ = nat_succI RSN (2,add_commute);
   1.209 +
   1.210 +val prems = goal ListFn.thy
   1.211 +    "xs: list(A) ==> length(rev(xs)) = length(xs)";
   1.212 +by (list_ind_tac "xs" prems 1);
   1.213 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
   1.214 +val length_rev = result();
   1.215 +
   1.216 +val prems = goal ListFn.thy
   1.217 +    "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
   1.218 +by (list_ind_tac "ls" prems 1);
   1.219 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
   1.220 +val length_flat = result();
   1.221 +
   1.222 +(*** theorems about app ***)
   1.223 +
   1.224 +val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
   1.225 +by (rtac (major RS List.induct) 1);
   1.226 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.227 +val app_right_Nil = result();
   1.228 +
   1.229 +val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
   1.230 +by (list_ind_tac "xs" prems 1);
   1.231 +by (ALLGOALS (ASM_SIMP_TAC list_ss));
   1.232 +val app_assoc = result();
   1.233 +
   1.234 +val prems = goal ListFn.thy
   1.235 +    "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
   1.236 +by (list_ind_tac "ls" prems 1);
   1.237 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
   1.238 +val flat_app_distrib = result();
   1.239 +
   1.240 +(*** theorems about rev ***)
   1.241 +
   1.242 +val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
   1.243 +by (list_ind_tac "l" prems 1);
   1.244 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
   1.245 +val rev_map_distrib = result();
   1.246 +
   1.247 +(*Simplifier needs the premises as assumptions because rewriting will not
   1.248 +  instantiate the variable ?A in the rules' typing conditions; note that
   1.249 +  rev_type does not instantiate ?A.  Only the premises do.
   1.250 +*)
   1.251 +val prems = goal ListFn.thy
   1.252 +    "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
   1.253 +by (cut_facts_tac prems 1);
   1.254 +by (etac List.induct 1);
   1.255 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
   1.256 +val rev_app_distrib = result();
   1.257 +
   1.258 +val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
   1.259 +by (list_ind_tac "l" prems 1);
   1.260 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
   1.261 +val rev_rev_ident = result();
   1.262 +
   1.263 +val prems = goal ListFn.thy
   1.264 +    "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
   1.265 +by (list_ind_tac "ls" prems 1);
   1.266 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews 
   1.267 +       [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
   1.268 +val rev_flat = result();
   1.269 +
   1.270 +
   1.271 +(*** theorems about list_add ***)
   1.272 +
   1.273 +val prems = goal ListFn.thy
   1.274 +    "[| xs: list(nat);  ys: list(nat) |] ==> \
   1.275 +\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
   1.276 +by (cut_facts_tac prems 1);
   1.277 +by (list_ind_tac "xs" prems 1);
   1.278 +by (ALLGOALS 
   1.279 +    (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
   1.280 +by (resolve_tac arith_congs 1);
   1.281 +by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
   1.282 +val list_add_app = result();
   1.283 +
   1.284 +val prems = goal ListFn.thy
   1.285 +    "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
   1.286 +by (list_ind_tac "l" prems 1);
   1.287 +by (ALLGOALS
   1.288 +    (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
   1.289 +val list_add_rev = result();
   1.290 +
   1.291 +val prems = goal ListFn.thy
   1.292 +    "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
   1.293 +by (list_ind_tac "ls" prems 1);
   1.294 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
   1.295 +by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
   1.296 +val list_add_flat = result();
   1.297 +
   1.298 +(** New induction rule **)
   1.299 +
   1.300 +val major::prems = goal ListFn.thy
   1.301 +    "[| l: list(A);  \
   1.302 +\       P(Nil);        \
   1.303 +\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
   1.304 +\    |] ==> P(l)";
   1.305 +by (rtac (major RS rev_rev_ident RS subst) 1);
   1.306 +by (rtac (major RS rev_type RS List.induct) 1);
   1.307 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
   1.308 +val list_append_induct = result();
   1.309 +