0

1 
(* Title: ZF/listfn.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
For listfn.thy. Lists in ZermeloFraenkel Set Theory


7 
*)


8 


9 
open ListFn;


10 


11 


12 
(** list_rec  by Vset recursion **)


13 


14 
(*Used to verify list_rec*)


15 
val list_rec_ss = ZF_ss


16 
addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])


17 
addrews List.case_eqns;


18 


19 
goal ListFn.thy "list_rec(Nil,c,h) = c";


20 
by (rtac (list_rec_def RS def_Vrec RS trans) 1);


21 
by (SIMP_TAC list_rec_ss 1);


22 
val list_rec_Nil = result();


23 


24 
goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";


25 
by (rtac (list_rec_def RS def_Vrec RS trans) 1);


26 
by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);


27 
val list_rec_Cons = result();


28 


29 
(*Type checking  proved by induction, as usual*)


30 
val prems = goal ListFn.thy


31 
"[ l: list(A); \


32 
\ c: C(Nil); \


33 
\ !!x y r. [ x:A; y: list(A); r: C(y) ] ==> h(x,y,r): C(Cons(x,y)) \


34 
\ ] ==> list_rec(l,c,h) : C(l)";


35 
by (list_ind_tac "l" prems 1);


36 
by (ALLGOALS (ASM_SIMP_TAC


37 
(ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));


38 
val list_rec_type = result();


39 


40 
(** Versions for use with definitions **)


41 


42 
val [rew] = goal ListFn.thy


43 
"[ !!l. j(l)==list_rec(l, c, h) ] ==> j(Nil) = c";


44 
by (rewtac rew);


45 
by (rtac list_rec_Nil 1);


46 
val def_list_rec_Nil = result();


47 


48 
val [rew] = goal ListFn.thy


49 
"[ !!l. j(l)==list_rec(l, c, h) ] ==> j(Cons(a,l)) = h(a,l,j(l))";


50 
by (rewtac rew);


51 
by (rtac list_rec_Cons 1);


52 
val def_list_rec_Cons = result();


53 


54 
fun list_recs def = map standard


55 
([def] RL [def_list_rec_Nil, def_list_rec_Cons]);


56 


57 
(** map **)


58 


59 
val [map_Nil,map_Cons] = list_recs map_def;


60 


61 
val prems = goalw ListFn.thy [map_def]


62 
"[ l: list(A); !!x. x: A ==> h(x): B ] ==> map(h,l) : list(B)";


63 
by (REPEAT (ares_tac (prems@[list_rec_type, NilI, ConsI]) 1));


64 
val map_type = result();


65 


66 
val [major] = goal ListFn.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";


67 
by (rtac (major RS map_type) 1);


68 
by (etac RepFunI 1);


69 
val map_type2 = result();


70 


71 
(** length **)


72 


73 
val [length_Nil,length_Cons] = list_recs length_def;


74 


75 
val prems = goalw ListFn.thy [length_def]


76 
"l: list(A) ==> length(l) : nat";


77 
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1));


78 
val length_type = result();


79 


80 
(** app **)


81 


82 
val [app_Nil,app_Cons] = list_recs app_def;


83 


84 
val prems = goalw ListFn.thy [app_def]


85 
"[ xs: list(A); ys: list(A) ] ==> xs@ys : list(A)";


86 
by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1));


87 
val app_type = result();


88 


89 
(** rev **)


90 


91 
val [rev_Nil,rev_Cons] = list_recs rev_def;


92 


93 
val prems = goalw ListFn.thy [rev_def]


94 
"xs: list(A) ==> rev(xs) : list(A)";


95 
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));


96 
val rev_type = result();


97 


98 


99 
(** flat **)


100 


101 
val [flat_Nil,flat_Cons] = list_recs flat_def;


102 


103 
val prems = goalw ListFn.thy [flat_def]


104 
"ls: list(list(A)) ==> flat(ls) : list(A)";


105 
by (REPEAT (ares_tac (prems @ [list_rec_type, NilI, ConsI, app_type]) 1));


106 
val flat_type = result();


107 


108 


109 
(** list_add **)


110 


111 
val [list_add_Nil,list_add_Cons] = list_recs list_add_def;


112 


113 
val prems = goalw ListFn.thy [list_add_def]


114 
"xs: list(nat) ==> list_add(xs) : nat";


115 
by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, add_type]) 1));


116 
val list_add_type = result();


117 


118 
(** ListFn simplification **)


119 


120 
val list_typechecks =


121 
[NilI, ConsI, list_rec_type,


122 
map_type, map_type2, app_type, length_type, rev_type, flat_type,


123 
list_add_type];


124 


125 
val list_congs =


126 
List.congs @


127 
mk_congs ListFn.thy


128 
["list_rec","map","op @","length","rev","flat","list_add"];


129 


130 
val list_ss = arith_ss


131 
addcongs list_congs


132 
addrews List.case_eqns


133 
addrews list_typechecks


134 
addrews [list_rec_Nil, list_rec_Cons,


135 
map_Nil, map_Cons,


136 
app_Nil, app_Cons,


137 
length_Nil, length_Cons,


138 
rev_Nil, rev_Cons,


139 
flat_Nil, flat_Cons,


140 
list_add_Nil, list_add_Cons];


141 


142 
(*** theorems about map ***)


143 


144 
val prems = goal ListFn.thy


145 
"l: list(A) ==> map(%u.u, l) = l";


146 
by (list_ind_tac "l" prems 1);


147 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


148 
val map_ident = result();


149 


150 
val prems = goal ListFn.thy


151 
"l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";


152 
by (list_ind_tac "l" prems 1);


153 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


154 
val map_compose = result();


155 


156 
val prems = goal ListFn.thy


157 
"xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";


158 
by (list_ind_tac "xs" prems 1);


159 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


160 
val map_app_distrib = result();


161 


162 
val prems = goal ListFn.thy


163 
"ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";


164 
by (list_ind_tac "ls" prems 1);


165 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));


166 
val map_flat = result();


167 


168 
val prems = goal ListFn.thy


169 
"l: list(A) ==> \


170 
\ list_rec(map(h,l), c, d) = \


171 
\ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";


172 
by (list_ind_tac "l" prems 1);


173 
by (ALLGOALS


174 
(ASM_SIMP_TAC


175 
(list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));


176 
val list_rec_map = result();


177 


178 
(** theorems about list(Collect(A,P))  used in ex/term.ML **)


179 


180 
(* c : list(Collect(B,P)) ==> c : list(B) *)


181 
val list_CollectD = standard (Collect_subset RS list_mono RS subsetD);


182 


183 
val prems = goal ListFn.thy


184 
"l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";


185 
by (list_ind_tac "l" prems 1);


186 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


187 
val map_list_Collect = result();


188 


189 
(*** theorems about length ***)


190 


191 
val prems = goal ListFn.thy


192 
"xs: list(A) ==> length(map(h,xs)) = length(xs)";


193 
by (list_ind_tac "xs" prems 1);


194 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


195 
val length_map = result();


196 


197 
val prems = goal ListFn.thy


198 
"xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";


199 
by (list_ind_tac "xs" prems 1);


200 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


201 
val length_app = result();


202 


203 
(* [ m: nat; n: nat ] ==> m #+ succ(n) = succ(n) #+ m


204 
Used for rewriting below*)


205 
val add_commute_succ = nat_succI RSN (2,add_commute);


206 


207 
val prems = goal ListFn.thy


208 
"xs: list(A) ==> length(rev(xs)) = length(xs)";


209 
by (list_ind_tac "xs" prems 1);


210 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));


211 
val length_rev = result();


212 


213 
val prems = goal ListFn.thy


214 
"ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";


215 
by (list_ind_tac "ls" prems 1);


216 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));


217 
val length_flat = result();


218 


219 
(*** theorems about app ***)


220 


221 
val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";


222 
by (rtac (major RS List.induct) 1);


223 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


224 
val app_right_Nil = result();


225 


226 
val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";


227 
by (list_ind_tac "xs" prems 1);


228 
by (ALLGOALS (ASM_SIMP_TAC list_ss));


229 
val app_assoc = result();


230 


231 
val prems = goal ListFn.thy


232 
"ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";


233 
by (list_ind_tac "ls" prems 1);


234 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));


235 
val flat_app_distrib = result();


236 


237 
(*** theorems about rev ***)


238 


239 
val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";


240 
by (list_ind_tac "l" prems 1);


241 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));


242 
val rev_map_distrib = result();


243 


244 
(*Simplifier needs the premises as assumptions because rewriting will not


245 
instantiate the variable ?A in the rules' typing conditions; note that


246 
rev_type does not instantiate ?A. Only the premises do.


247 
*)


248 
val prems = goal ListFn.thy


249 
"[ xs: list(A); ys: list(A) ] ==> rev(xs@ys) = rev(ys)@rev(xs)";


250 
by (cut_facts_tac prems 1);


251 
by (etac List.induct 1);


252 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));


253 
val rev_app_distrib = result();


254 


255 
val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";


256 
by (list_ind_tac "l" prems 1);


257 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));


258 
val rev_rev_ident = result();


259 


260 
val prems = goal ListFn.thy


261 
"ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";


262 
by (list_ind_tac "ls" prems 1);


263 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews


264 
[map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));


265 
val rev_flat = result();


266 


267 


268 
(*** theorems about list_add ***)


269 


270 
val prems = goal ListFn.thy


271 
"[ xs: list(nat); ys: list(nat) ] ==> \


272 
\ list_add(xs@ys) = list_add(ys) #+ list_add(xs)";


273 
by (cut_facts_tac prems 1);


274 
by (list_ind_tac "xs" prems 1);


275 
by (ALLGOALS


276 
(ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));


277 
by (resolve_tac arith_congs 1);


278 
by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));


279 
val list_add_app = result();


280 


281 
val prems = goal ListFn.thy


282 
"l: list(nat) ==> list_add(rev(l)) = list_add(l)";


283 
by (list_ind_tac "l" prems 1);


284 
by (ALLGOALS


285 
(ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));


286 
val list_add_rev = result();


287 


288 
val prems = goal ListFn.thy


289 
"ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";


290 
by (list_ind_tac "ls" prems 1);


291 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));


292 
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));


293 
val list_add_flat = result();


294 


295 
(** New induction rule **)


296 


297 
val major::prems = goal ListFn.thy


298 
"[ l: list(A); \


299 
\ P(Nil); \


300 
\ !!x y. [ x: A; y: list(A); P(y) ] ==> P(y @ [x]) \


301 
\ ] ==> P(l)";


302 
by (rtac (major RS rev_rev_ident RS subst) 1);


303 
by (rtac (major RS rev_type RS List.induct) 1);


304 
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));


305 
val list_append_induct = result();


306 
