author | regensbu |
Fri, 06 Oct 1995 16:17:08 +0100 | |
changeset 1273 | 6960ec882bca |
parent 1264 | 3eb91524b938 |
child 1301 | 42782316d510 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/List |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1994 TU Muenchen |
|
5 |
||
6 |
List lemmas |
|
7 |
*) |
|
8 |
||
9 |
open List; |
|
10 |
||
11 |
val [Nil_not_Cons,Cons_not_Nil] = list.distinct; |
|
12 |
||
13 |
bind_thm("Cons_neq_Nil", Cons_not_Nil RS notE); |
|
14 |
bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil); |
|
15 |
||
16 |
bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE); |
|
17 |
||
18 |
goal List.thy "!x. xs ~= x#xs"; |
|
19 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
20 |
by (ALLGOALS Asm_simp_tac); |
923 | 21 |
qed "not_Cons_self"; |
22 |
||
23 |
goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)"; |
|
24 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
25 |
by (Simp_tac 1); |
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
26 |
by (Asm_simp_tac 1); |
1169 | 27 |
by (REPEAT(resolve_tac [exI,refl,conjI] 1)); |
923 | 28 |
qed "neq_Nil_conv"; |
29 |
||
30 |
||
31 |
(** @ - append **) |
|
32 |
||
33 |
goal List.thy "(xs@ys)@zs = xs@(ys@zs)"; |
|
34 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
35 |
by (ALLGOALS Asm_simp_tac); |
923 | 36 |
qed "append_assoc"; |
37 |
||
38 |
goal List.thy "xs @ [] = xs"; |
|
39 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
40 |
by (ALLGOALS Asm_simp_tac); |
923 | 41 |
qed "append_Nil2"; |
42 |
||
43 |
goal List.thy "(xs@ys = []) = (xs=[] & ys=[])"; |
|
44 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
45 |
by (ALLGOALS Asm_simp_tac); |
923 | 46 |
qed "append_is_Nil"; |
47 |
||
48 |
goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)"; |
|
49 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
50 |
by (ALLGOALS Asm_simp_tac); |
923 | 51 |
qed "same_append_eq"; |
52 |
||
53 |
||
1169 | 54 |
(** rev **) |
55 |
||
56 |
goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)"; |
|
57 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
58 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc]))); |
1169 | 59 |
qed "rev_append"; |
60 |
||
61 |
goal List.thy "rev(rev l) = l"; |
|
62 |
by (list.induct_tac "l" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
63 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append]))); |
1169 | 64 |
qed "rev_rev_ident"; |
65 |
||
66 |
||
923 | 67 |
(** mem **) |
68 |
||
69 |
goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; |
|
70 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
71 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
923 | 72 |
qed "mem_append"; |
73 |
||
74 |
goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; |
|
75 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
76 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
923 | 77 |
qed "mem_filter"; |
78 |
||
79 |
(** list_all **) |
|
80 |
||
81 |
goal List.thy "(Alls x:xs.True) = True"; |
|
82 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
83 |
by (ALLGOALS Asm_simp_tac); |
923 | 84 |
qed "list_all_True"; |
85 |
||
86 |
goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; |
|
87 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
88 |
by (ALLGOALS Asm_simp_tac); |
923 | 89 |
qed "list_all_conj"; |
90 |
||
91 |
goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; |
|
92 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
93 |
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
1169 | 94 |
by (fast_tac HOL_cs 1); |
923 | 95 |
qed "list_all_mem_conv"; |
96 |
||
97 |
||
98 |
(** list_case **) |
|
99 |
||
100 |
goal List.thy |
|
101 |
"P(list_case a f xs) = ((xs=[] --> P(a)) & \ |
|
102 |
\ (!y ys. xs=y#ys --> P(f y ys)))"; |
|
103 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
104 |
by (ALLGOALS Asm_simp_tac); |
1169 | 105 |
by (fast_tac HOL_cs 1); |
923 | 106 |
qed "expand_list_case"; |
107 |
||
108 |
goal List.thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)"; |
|
1169 | 109 |
by (list.induct_tac "xs" 1); |
110 |
by (fast_tac HOL_cs 1); |
|
111 |
by (fast_tac HOL_cs 1); |
|
923 | 112 |
bind_thm("list_eq_cases", |
113 |
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp)))))); |
|
114 |
||
115 |
(** flat **) |
|
116 |
||
117 |
goal List.thy "flat(xs@ys) = flat(xs)@flat(ys)"; |
|
118 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
119 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_assoc]))); |
923 | 120 |
qed"flat_append"; |
121 |
||
962 | 122 |
(** length **) |
123 |
||
124 |
goal List.thy "length(xs@ys) = length(xs)+length(ys)"; |
|
125 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
126 |
by (ALLGOALS Asm_simp_tac); |
962 | 127 |
qed"length_append"; |
128 |
||
1169 | 129 |
goal List.thy "length(rev xs) = length(xs)"; |
130 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
131 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [length_append]))); |
1169 | 132 |
qed "length_rev"; |
133 |
||
923 | 134 |
(** nth **) |
135 |
||
136 |
val [nth_0,nth_Suc] = nat_recs nth_def; |
|
137 |
store_thm("nth_0",nth_0); |
|
138 |
store_thm("nth_Suc",nth_Suc); |
|
139 |
||
140 |
(** Additional mapping lemmas **) |
|
141 |
||
995
95c148a7b9c4
generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)
nipkow
parents:
974
diff
changeset
|
142 |
goal List.thy "map (%x.x) = (%xs.xs)"; |
95c148a7b9c4
generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)
nipkow
parents:
974
diff
changeset
|
143 |
by (rtac ext 1); |
923 | 144 |
by (list.induct_tac "xs" 1); |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
145 |
by (ALLGOALS Asm_simp_tac); |
923 | 146 |
qed "map_ident"; |
147 |
||
148 |
goal List.thy "map f (xs@ys) = map f xs @ map f ys"; |
|
149 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
150 |
by (ALLGOALS Asm_simp_tac); |
923 | 151 |
qed "map_append"; |
152 |
||
153 |
goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)"; |
|
154 |
by (list.induct_tac "xs" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
155 |
by (ALLGOALS Asm_simp_tac); |
923 | 156 |
qed "map_compose"; |
157 |
||
1169 | 158 |
goal List.thy "rev(map f l) = map f (rev l)"; |
159 |
by (list.induct_tac "l" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
160 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append]))); |
1169 | 161 |
qed "rev_map_distrib"; |
162 |
||
163 |
goal List.thy "rev(flat ls) = flat (map rev (rev ls))"; |
|
164 |
by (list.induct_tac "ls" 1); |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
165 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps |
1169 | 166 |
[map_append, flat_append, rev_append, append_Nil2]))); |
167 |
qed "rev_flat"; |
|
168 |
||
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1202
diff
changeset
|
169 |
Addsimps |
923 | 170 |
[not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq, |
171 |
mem_append, mem_filter, |
|
1202 | 172 |
rev_append, rev_rev_ident, |
923 | 173 |
map_ident, map_append, map_compose, |
962 | 174 |
flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc]; |
923 | 175 |