22 by (ALLGOALS (asm_simp_tac list_ss)); |
22 by (ALLGOALS (asm_simp_tac list_ss)); |
23 qed "not_Cons_self"; |
23 qed "not_Cons_self"; |
24 |
24 |
25 goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)"; |
25 goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)"; |
26 by (list.induct_tac "xs" 1); |
26 by (list.induct_tac "xs" 1); |
27 by(simp_tac list_ss 1); |
27 by (simp_tac list_ss 1); |
28 by(asm_simp_tac list_ss 1); |
28 by (asm_simp_tac list_ss 1); |
29 by(REPEAT(resolve_tac [exI,refl,conjI] 1)); |
29 by (REPEAT(resolve_tac [exI,refl,conjI] 1)); |
30 qed "neq_Nil_conv"; |
30 qed "neq_Nil_conv"; |
31 |
31 |
32 val list_ss = arith_ss addsimps list.simps @ |
32 val list_ss = arith_ss addsimps list.simps @ |
33 [null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons, |
33 [null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons, |
34 mem_Nil, mem_Cons, |
34 mem_Nil, mem_Cons, |
35 append_Nil, append_Cons, |
35 append_Nil, append_Cons, |
|
36 rev_Nil, rev_Cons, |
36 map_Nil, map_Cons, |
37 map_Nil, map_Cons, |
37 flat_Nil, flat_Cons, |
38 flat_Nil, flat_Cons, |
38 list_all_Nil, list_all_Cons, |
39 list_all_Nil, list_all_Cons, |
39 filter_Nil, filter_Cons, |
40 filter_Nil, filter_Cons, |
40 foldl_Nil, foldl_Cons, |
41 foldl_Nil, foldl_Cons, |
43 |
44 |
44 (** @ - append **) |
45 (** @ - append **) |
45 |
46 |
46 goal List.thy "(xs@ys)@zs = xs@(ys@zs)"; |
47 goal List.thy "(xs@ys)@zs = xs@(ys@zs)"; |
47 by (list.induct_tac "xs" 1); |
48 by (list.induct_tac "xs" 1); |
48 by(ALLGOALS(asm_simp_tac list_ss)); |
49 by (ALLGOALS (asm_simp_tac list_ss)); |
49 qed "append_assoc"; |
50 qed "append_assoc"; |
50 |
51 |
51 goal List.thy "xs @ [] = xs"; |
52 goal List.thy "xs @ [] = xs"; |
52 by (list.induct_tac "xs" 1); |
53 by (list.induct_tac "xs" 1); |
53 by(ALLGOALS(asm_simp_tac list_ss)); |
54 by (ALLGOALS (asm_simp_tac list_ss)); |
54 qed "append_Nil2"; |
55 qed "append_Nil2"; |
55 |
56 |
56 goal List.thy "(xs@ys = []) = (xs=[] & ys=[])"; |
57 goal List.thy "(xs@ys = []) = (xs=[] & ys=[])"; |
57 by (list.induct_tac "xs" 1); |
58 by (list.induct_tac "xs" 1); |
58 by(ALLGOALS(asm_simp_tac list_ss)); |
59 by (ALLGOALS (asm_simp_tac list_ss)); |
59 qed "append_is_Nil"; |
60 qed "append_is_Nil"; |
60 |
61 |
61 goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)"; |
62 goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)"; |
62 by (list.induct_tac "xs" 1); |
63 by (list.induct_tac "xs" 1); |
63 by(ALLGOALS(asm_simp_tac list_ss)); |
64 by (ALLGOALS (asm_simp_tac list_ss)); |
64 qed "same_append_eq"; |
65 qed "same_append_eq"; |
|
66 |
|
67 |
|
68 (** rev **) |
|
69 |
|
70 goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)"; |
|
71 by (list.induct_tac "xs" 1); |
|
72 by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_Nil2,append_assoc]))); |
|
73 qed "rev_append"; |
|
74 |
|
75 goal List.thy "rev(rev l) = l"; |
|
76 by (list.induct_tac "l" 1); |
|
77 by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_append]))); |
|
78 qed "rev_rev_ident"; |
65 |
79 |
66 |
80 |
67 (** mem **) |
81 (** mem **) |
68 |
82 |
69 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; |
83 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; |
70 by (list.induct_tac "xs" 1); |
84 by (list.induct_tac "xs" 1); |
71 by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); |
85 by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if])))); |
72 qed "mem_append"; |
86 qed "mem_append"; |
73 |
87 |
74 goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; |
88 goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; |
75 by (list.induct_tac "xs" 1); |
89 by (list.induct_tac "xs" 1); |
76 by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); |
90 by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if])))); |
77 qed "mem_filter"; |
91 qed "mem_filter"; |
78 |
92 |
79 (** list_all **) |
93 (** list_all **) |
80 |
94 |
81 goal List.thy "(Alls x:xs.True) = True"; |
95 goal List.thy "(Alls x:xs.True) = True"; |
82 by (list.induct_tac "xs" 1); |
96 by (list.induct_tac "xs" 1); |
83 by(ALLGOALS(asm_simp_tac list_ss)); |
97 by (ALLGOALS (asm_simp_tac list_ss)); |
84 qed "list_all_True"; |
98 qed "list_all_True"; |
85 |
99 |
86 goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
100 goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
87 by (list.induct_tac "xs" 1); |
101 by (list.induct_tac "xs" 1); |
88 by(ALLGOALS(asm_simp_tac list_ss)); |
102 by (ALLGOALS (asm_simp_tac list_ss)); |
89 qed "list_all_conj"; |
103 qed "list_all_conj"; |
90 |
104 |
91 goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; |
105 goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; |
92 by (list.induct_tac "xs" 1); |
106 by (list.induct_tac "xs" 1); |
93 by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); |
107 by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if])))); |
94 by(fast_tac HOL_cs 1); |
108 by (fast_tac HOL_cs 1); |
95 qed "list_all_mem_conv"; |
109 qed "list_all_mem_conv"; |
96 |
110 |
97 |
111 |
98 (** list_case **) |
112 (** list_case **) |
99 |
113 |
100 goal List.thy |
114 goal List.thy |
101 "P(list_case a f xs) = ((xs=[] --> P(a)) & \ |
115 "P(list_case a f xs) = ((xs=[] --> P(a)) & \ |
102 \ (!y ys. xs=y#ys --> P(f y ys)))"; |
116 \ (!y ys. xs=y#ys --> P(f y ys)))"; |
103 by (list.induct_tac "xs" 1); |
117 by (list.induct_tac "xs" 1); |
104 by(ALLGOALS(asm_simp_tac list_ss)); |
118 by (ALLGOALS (asm_simp_tac list_ss)); |
105 by(fast_tac HOL_cs 1); |
119 by (fast_tac HOL_cs 1); |
106 qed "expand_list_case"; |
120 qed "expand_list_case"; |
107 |
121 |
108 goal List.thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; |
122 goal List.thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; |
109 by(list.induct_tac "xs" 1); |
123 by (list.induct_tac "xs" 1); |
110 by(fast_tac HOL_cs 1); |
124 by (fast_tac HOL_cs 1); |
111 by(fast_tac HOL_cs 1); |
125 by (fast_tac HOL_cs 1); |
112 bind_thm("list_eq_cases", |
126 bind_thm("list_eq_cases", |
113 impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp)))))); |
127 impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp)))))); |
114 |
128 |
115 (** flat **) |
129 (** flat **) |
116 |
130 |
117 goal List.thy "flat(xs@ys) = flat(xs)@flat(ys)"; |
131 goal List.thy "flat(xs@ys) = flat(xs)@flat(ys)"; |
118 by (list.induct_tac "xs" 1); |
132 by (list.induct_tac "xs" 1); |
119 by(ALLGOALS(asm_simp_tac (list_ss addsimps [append_assoc]))); |
133 by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_assoc]))); |
120 qed"flat_append"; |
134 qed"flat_append"; |
121 |
135 |
122 (** length **) |
136 (** length **) |
123 |
137 |
124 goal List.thy "length(xs@ys) = length(xs)+length(ys)"; |
138 goal List.thy "length(xs@ys) = length(xs)+length(ys)"; |
125 by (list.induct_tac "xs" 1); |
139 by (list.induct_tac "xs" 1); |
126 by(ALLGOALS(asm_simp_tac list_ss)); |
140 by (ALLGOALS (asm_simp_tac list_ss)); |
127 qed"length_append"; |
141 qed"length_append"; |
|
142 |
|
143 goal List.thy "length(rev xs) = length(xs)"; |
|
144 by (list.induct_tac "xs" 1); |
|
145 by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_append]))); |
|
146 qed "length_rev"; |
128 |
147 |
129 (** nth **) |
148 (** nth **) |
130 |
149 |
131 val [nth_0,nth_Suc] = nat_recs nth_def; |
150 val [nth_0,nth_Suc] = nat_recs nth_def; |
132 store_thm("nth_0",nth_0); |
151 store_thm("nth_0",nth_0); |
148 goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)"; |
167 goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)"; |
149 by (list.induct_tac "xs" 1); |
168 by (list.induct_tac "xs" 1); |
150 by (ALLGOALS (asm_simp_tac list_ss)); |
169 by (ALLGOALS (asm_simp_tac list_ss)); |
151 qed "map_compose"; |
170 qed "map_compose"; |
152 |
171 |
|
172 goal List.thy "rev(map f l) = map f (rev l)"; |
|
173 by (list.induct_tac "l" 1); |
|
174 by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_append]))); |
|
175 qed "rev_map_distrib"; |
|
176 |
|
177 goal List.thy "rev(flat ls) = flat (map rev (rev ls))"; |
|
178 by (list.induct_tac "ls" 1); |
|
179 by (ALLGOALS (asm_simp_tac (list_ss addsimps |
|
180 [map_append, flat_append, rev_append, append_Nil2]))); |
|
181 qed "rev_flat"; |
|
182 |
153 val list_ss = list_ss addsimps |
183 val list_ss = list_ss addsimps |
154 [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq, |
184 [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq, |
155 mem_append, mem_filter, |
185 mem_append, mem_filter, |
156 map_ident, map_append, map_compose, |
186 map_ident, map_append, map_compose, |
157 flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc]; |
187 flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc]; |