30 |
31 |
31 goal List.thy "(xs@ys)@zs = xs@(ys@zs)"; |
32 goal List.thy "(xs@ys)@zs = xs@(ys@zs)"; |
32 by (list.induct_tac "xs" 1); |
33 by (list.induct_tac "xs" 1); |
33 by (ALLGOALS Asm_simp_tac); |
34 by (ALLGOALS Asm_simp_tac); |
34 qed "append_assoc"; |
35 qed "append_assoc"; |
|
36 Addsimps [append_assoc]; |
35 |
37 |
36 goal List.thy "xs @ [] = xs"; |
38 goal List.thy "xs @ [] = xs"; |
37 by (list.induct_tac "xs" 1); |
39 by (list.induct_tac "xs" 1); |
38 by (ALLGOALS Asm_simp_tac); |
40 by (ALLGOALS Asm_simp_tac); |
39 qed "append_Nil2"; |
41 qed "append_Nil2"; |
|
42 Addsimps [append_Nil2]; |
40 |
43 |
41 goal List.thy "(xs@ys = []) = (xs=[] & ys=[])"; |
44 goal List.thy "(xs@ys = []) = (xs=[] & ys=[])"; |
42 by (list.induct_tac "xs" 1); |
45 by (list.induct_tac "xs" 1); |
43 by (ALLGOALS Asm_simp_tac); |
46 by (ALLGOALS Asm_simp_tac); |
44 qed "append_is_Nil"; |
47 qed "append_is_Nil"; |
|
48 Addsimps [append_is_Nil]; |
45 |
49 |
46 goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)"; |
50 goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)"; |
47 by (list.induct_tac "xs" 1); |
51 by (list.induct_tac "xs" 1); |
48 by (ALLGOALS Asm_simp_tac); |
52 by (ALLGOALS Asm_simp_tac); |
49 qed "same_append_eq"; |
53 qed "same_append_eq"; |
|
54 Addsimps [same_append_eq]; |
50 |
55 |
51 goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)"; |
56 goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)"; |
52 by (list.induct_tac "xs" 1); |
57 by (list.induct_tac "xs" 1); |
53 by (ALLGOALS Asm_simp_tac); |
58 by (ALLGOALS Asm_simp_tac); |
54 qed "hd_append"; |
59 qed "hd_append"; |
55 |
60 |
56 (** rev **) |
61 (** rev **) |
57 |
62 |
58 goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)"; |
63 goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)"; |
59 by (list.induct_tac "xs" 1); |
64 by (list.induct_tac "xs" 1); |
60 by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc]))); |
65 by (ALLGOALS Asm_simp_tac); |
61 qed "rev_append"; |
66 qed "rev_append"; |
|
67 Addsimps[rev_append]; |
62 |
68 |
63 goal List.thy "rev(rev l) = l"; |
69 goal List.thy "rev(rev l) = l"; |
64 by (list.induct_tac "l" 1); |
70 by (list.induct_tac "l" 1); |
65 by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append]))); |
71 by (ALLGOALS Asm_simp_tac); |
66 qed "rev_rev_ident"; |
72 qed "rev_rev_ident"; |
67 |
73 Addsimps[rev_rev_ident]; |
68 |
74 |
69 (** mem **) |
75 (** mem **) |
70 |
76 |
71 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; |
77 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; |
72 by (list.induct_tac "xs" 1); |
78 by (list.induct_tac "xs" 1); |
73 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
79 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
74 qed "mem_append"; |
80 qed "mem_append"; |
|
81 Addsimps[mem_append]; |
75 |
82 |
76 goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; |
83 goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; |
77 by (list.induct_tac "xs" 1); |
84 by (list.induct_tac "xs" 1); |
78 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
85 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
79 qed "mem_filter"; |
86 qed "mem_filter"; |
|
87 Addsimps[mem_filter]; |
80 |
88 |
81 (** set_of_list **) |
89 (** set_of_list **) |
82 |
90 |
83 goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)"; |
91 goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)"; |
84 by (list.induct_tac "xs" 1); |
92 by (list.induct_tac "xs" 1); |
85 by (ALLGOALS Asm_simp_tac); |
93 by (ALLGOALS Asm_simp_tac); |
86 by (Fast_tac 1); |
94 by (Fast_tac 1); |
87 qed "set_of_list_append"; |
95 qed "set_of_list_append"; |
|
96 Addsimps[set_of_list_append]; |
88 |
97 |
89 goal thy "(x mem xs) = (x: set_of_list xs)"; |
98 goal thy "(x mem xs) = (x: set_of_list xs)"; |
90 by (list.induct_tac "xs" 1); |
99 by (list.induct_tac "xs" 1); |
91 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
100 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
92 by (Fast_tac 1); |
101 by (Fast_tac 1); |
98 qed "set_of_list_subset_Cons"; |
107 qed "set_of_list_subset_Cons"; |
99 |
108 |
100 |
109 |
101 (** list_all **) |
110 (** list_all **) |
102 |
111 |
103 goal List.thy "(Alls x:xs.True) = True"; |
112 goal List.thy "list_all (%x.True) xs = True"; |
104 by (list.induct_tac "xs" 1); |
113 by (list.induct_tac "xs" 1); |
105 by (ALLGOALS Asm_simp_tac); |
114 by (ALLGOALS Asm_simp_tac); |
106 qed "list_all_True"; |
115 qed "list_all_True"; |
|
116 Addsimps [list_all_True]; |
107 |
117 |
108 goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
118 goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
109 by (list.induct_tac "xs" 1); |
119 by (list.induct_tac "xs" 1); |
110 by (ALLGOALS Asm_simp_tac); |
120 by (ALLGOALS Asm_simp_tac); |
111 qed "list_all_conj"; |
121 qed "list_all_append"; |
112 |
122 Addsimps [list_all_append]; |
113 goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; |
123 |
|
124 goal List.thy "list_all P xs = (!x. x mem xs --> P(x))"; |
114 by (list.induct_tac "xs" 1); |
125 by (list.induct_tac "xs" 1); |
115 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
126 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
116 by (Fast_tac 1); |
127 by (Fast_tac 1); |
117 qed "list_all_mem_conv"; |
128 qed "list_all_mem_conv"; |
118 |
129 |
125 by (list.induct_tac "xs" 1); |
136 by (list.induct_tac "xs" 1); |
126 by (ALLGOALS Asm_simp_tac); |
137 by (ALLGOALS Asm_simp_tac); |
127 by (Fast_tac 1); |
138 by (Fast_tac 1); |
128 qed "expand_list_case"; |
139 qed "expand_list_case"; |
129 |
140 |
|
141 val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)"; |
|
142 by(list.induct_tac "xs" 1); |
|
143 by(REPEAT(resolve_tac prems 1)); |
|
144 qed "list_cases"; |
|
145 |
130 goal List.thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; |
146 goal List.thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; |
131 by (list.induct_tac "xs" 1); |
147 by (list.induct_tac "xs" 1); |
132 by (Fast_tac 1); |
148 by (Fast_tac 1); |
133 by (Fast_tac 1); |
149 by (Fast_tac 1); |
134 bind_thm("list_eq_cases", |
150 bind_thm("list_eq_cases", |
236 goal List.thy "map (%x.x) = (%xs.xs)"; |
253 goal List.thy "map (%x.x) = (%xs.xs)"; |
237 by (rtac ext 1); |
254 by (rtac ext 1); |
238 by (list.induct_tac "xs" 1); |
255 by (list.induct_tac "xs" 1); |
239 by (ALLGOALS Asm_simp_tac); |
256 by (ALLGOALS Asm_simp_tac); |
240 qed "map_ident"; |
257 qed "map_ident"; |
|
258 Addsimps[map_ident]; |
241 |
259 |
242 goal List.thy "map f (xs@ys) = map f xs @ map f ys"; |
260 goal List.thy "map f (xs@ys) = map f xs @ map f ys"; |
243 by (list.induct_tac "xs" 1); |
261 by (list.induct_tac "xs" 1); |
244 by (ALLGOALS Asm_simp_tac); |
262 by (ALLGOALS Asm_simp_tac); |
245 qed "map_append"; |
263 qed "map_append"; |
|
264 Addsimps[map_append]; |
246 |
265 |
247 goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)"; |
266 goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)"; |
248 by (list.induct_tac "xs" 1); |
267 by (list.induct_tac "xs" 1); |
249 by (ALLGOALS Asm_simp_tac); |
268 by (ALLGOALS Asm_simp_tac); |
250 qed "map_compose"; |
269 qed "map_compose"; |
|
270 Addsimps[map_compose]; |
251 |
271 |
252 goal List.thy "rev(map f l) = map f (rev l)"; |
272 goal List.thy "rev(map f l) = map f (rev l)"; |
253 by (list.induct_tac "l" 1); |
273 by (list.induct_tac "l" 1); |
254 by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append]))); |
274 by (ALLGOALS Asm_simp_tac); |
255 qed "rev_map_distrib"; |
275 qed "rev_map_distrib"; |
256 |
276 |
257 goal List.thy "rev(flat ls) = flat (map rev (rev ls))"; |
277 goal List.thy "rev(flat ls) = flat (map rev (rev ls))"; |
258 by (list.induct_tac "ls" 1); |
278 by (list.induct_tac "ls" 1); |
259 by (ALLGOALS (asm_simp_tac (!simpset addsimps |
279 by (ALLGOALS Asm_simp_tac); |
260 [map_append, flat_append, rev_append, append_Nil2]))); |
|
261 qed "rev_flat"; |
280 qed "rev_flat"; |
262 |
|
263 Addsimps |
|
264 [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq, |
|
265 mem_append, mem_filter, |
|
266 rev_append, rev_rev_ident, |
|
267 map_ident, map_append, map_compose, |
|
268 flat_append, list_all_True, list_all_conj]; |
|
269 |
|