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.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.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.113 +
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.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.127 +
1.128 +val list_congs =
1.129 +    List.congs @
1.130 +    mk_congs ListFn.thy
1.132 +
1.133 +val list_ss = arith_ss
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.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.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.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.272 +
1.273 +val prems = goal ListFn.thy
1.274 +    "[| xs: list(nat);  ys: list(nat) |] ==> \
1.276 +by (cut_facts_tac prems 1);
1.277 +by (list_ind_tac "xs" prems 1);
1.278 +by (ALLGOALS
1.280 +by (resolve_tac arith_congs 1);
1.283 +
1.284 +val prems = goal ListFn.thy
1.286 +by (list_ind_tac "l" prems 1);
1.287 +by (ALLGOALS
1.290 +
1.291 +val prems = goal ListFn.thy
1.293 +by (list_ind_tac "ls" prems 1);
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 +
```