author  paulson 
Tue, 02 Mar 2010 17:36:16 +0000  
changeset 35510  64d2d54cbf03 
parent 35296  975b34b6cf5b 
child 35603  c0db094d0d80 
permissions  rwrr 
13462  1 
(* Title: HOL/List.thy 
2 
Author: Tobias Nipkow 

923  3 
*) 
4 

13114  5 
header {* The datatype of finite lists *} 
13122  6 

15131  7 
theory List 
33593  8 
imports Plain Presburger ATP_Linkup Recdef 
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
31048
diff
changeset

9 
uses ("Tools/list_code.ML") 
15131  10 
begin 
923  11 

13142  12 
datatype 'a list = 
13366  13 
Nil ("[]") 
14 
 Cons 'a "'a list" (infixr "#" 65) 

923  15 

34941  16 
syntax 
17 
 {* list Enumeration *} 

35115  18 
"_list" :: "args => 'a list" ("[(_)]") 
34941  19 

20 
translations 

21 
"[x, xs]" == "x#[xs]" 

22 
"[x]" == "x#[]" 

23 

35115  24 

25 
subsection {* Basic list processing functions *} 

15302  26 

34941  27 
primrec 
28 
hd :: "'a list \<Rightarrow> 'a" where 

29 
"hd (x # xs) = x" 

30 

31 
primrec 

32 
tl :: "'a list \<Rightarrow> 'a list" where 

33 
"tl [] = []" 

34 
 "tl (x # xs) = xs" 

35 

36 
primrec 

37 
last :: "'a list \<Rightarrow> 'a" where 

38 
"last (x # xs) = (if xs = [] then x else last xs)" 

39 

40 
primrec 

41 
butlast :: "'a list \<Rightarrow> 'a list" where 

42 
"butlast []= []" 

43 
 "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)" 

44 

45 
primrec 

46 
set :: "'a list \<Rightarrow> 'a set" where 

47 
"set [] = {}" 

48 
 "set (x # xs) = insert x (set xs)" 

49 

50 
primrec 

51 
map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where 

52 
"map f [] = []" 

53 
 "map f (x # xs) = f x # map f xs" 

54 

55 
primrec 

56 
append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where 

57 
append_Nil:"[] @ ys = ys" 

58 
 append_Cons: "(x#xs) @ ys = x # xs @ ys" 

59 

60 
primrec 

61 
rev :: "'a list \<Rightarrow> 'a list" where 

62 
"rev [] = []" 

63 
 "rev (x # xs) = rev xs @ [x]" 

64 

65 
primrec 

66 
filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

67 
"filter P [] = []" 

68 
 "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)" 

69 

70 
syntax 

71 
 {* Special syntax for filter *} 

35115  72 
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<_./ _])") 
34941  73 

74 
translations 

75 
"[x<xs . P]"== "CONST filter (%x. P) xs" 

76 

77 
syntax (xsymbols) 

35115  78 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  79 
syntax (HTML output) 
35115  80 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  81 

82 
primrec 

83 
foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where 

84 
foldl_Nil: "foldl f a [] = a" 

85 
 foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs" 

86 

87 
primrec 

88 
foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where 

89 
"foldr f [] a = a" 

90 
 "foldr f (x # xs) a = f x (foldr f xs a)" 

91 

92 
primrec 

93 
concat:: "'a list list \<Rightarrow> 'a list" where 

94 
"concat [] = []" 

95 
 "concat (x # xs) = x @ concat xs" 

96 

97 
primrec (in monoid_add) 

98 
listsum :: "'a list \<Rightarrow> 'a" where 

99 
"listsum [] = 0" 

100 
 "listsum (x # xs) = x + listsum xs" 

101 

102 
primrec 

103 
drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

104 
drop_Nil: "drop n [] = []" 

105 
 drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs  Suc m \<Rightarrow> drop m xs)" 

106 
 {*Warning: simpset does not contain this definition, but separate 

107 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

108 

109 
primrec 

110 
take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

111 
take_Nil:"take n [] = []" 

112 
 take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> []  Suc m \<Rightarrow> x # take m xs)" 

113 
 {*Warning: simpset does not contain this definition, but separate 

114 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

115 

116 
primrec 

117 
nth :: "'a list => nat => 'a" (infixl "!" 100) where 

118 
nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x  Suc k \<Rightarrow> xs ! k)" 

119 
 {*Warning: simpset does not contain this definition, but separate 

120 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

121 

122 
primrec 

123 
list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 

124 
"list_update [] i v = []" 

125 
 "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs  Suc j \<Rightarrow> x # list_update xs j v)" 

923  126 

13146  127 
nonterminals lupdbinds lupdbind 
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

128 

923  129 
syntax 
13366  130 
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") 
131 
"" :: "lupdbind => lupdbinds" ("_") 

132 
"_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _") 

133 
"_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900) 

5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

134 

923  135 
translations 
35115  136 
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" 
34941  137 
"xs[i:=x]" == "CONST list_update xs i x" 
138 

139 
primrec 

140 
takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

141 
"takeWhile P [] = []" 

142 
 "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])" 

143 

144 
primrec 

145 
dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

146 
"dropWhile P [] = []" 

147 
 "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)" 

148 

149 
primrec 

150 
zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where 

151 
"zip xs [] = []" 

152 
 zip_Cons: "zip xs (y # ys) = (case xs of [] => []  z # zs => (z, y) # zip zs ys)" 

153 
 {*Warning: simpset does not contain this definition, but separate 

154 
theorems for @{text "xs = []"} and @{text "xs = z # zs"} *} 

155 

156 
primrec 

157 
upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where 

158 
upt_0: "[i..<0] = []" 

159 
 upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])" 

160 

161 
primrec 

162 
distinct :: "'a list \<Rightarrow> bool" where 

163 
"distinct [] \<longleftrightarrow> True" 

164 
 "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs" 

165 

166 
primrec 

167 
remdups :: "'a list \<Rightarrow> 'a list" where 

168 
"remdups [] = []" 

169 
 "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)" 

170 

34978
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

171 
definition 
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

172 
insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

173 
"insert x xs = (if x \<in> set xs then xs else x # xs)" 
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

174 

874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

175 
hide (open) const insert hide (open) fact insert_def 
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

176 

34941  177 
primrec 
178 
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

179 
"remove1 x [] = []" 

180 
 "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)" 

181 

182 
primrec 

183 
removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

184 
"removeAll x [] = []" 

185 
 "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)" 

186 

187 
primrec 

188 
replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 

189 
replicate_0: "replicate 0 x = []" 

190 
 replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

191 

13142  192 
text {* 
14589  193 
Function @{text size} is overloaded for all datatypes. Users may 
13366  194 
refer to the list version as @{text length}. *} 
13142  195 

19363  196 
abbreviation 
34941  197 
length :: "'a list \<Rightarrow> nat" where 
198 
"length \<equiv> size" 

15307  199 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

200 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

201 
rotate1 :: "'a list \<Rightarrow> 'a list" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

202 
"rotate1 xs = (case xs of [] \<Rightarrow> []  x#xs \<Rightarrow> xs @ [x])" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

203 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

204 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

205 
rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
30971  206 
"rotate n = rotate1 ^^ n" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

207 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

208 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

209 
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where 
28562  210 
[code del]: "list_all2 P xs ys = 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

211 
(length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

212 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

213 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

214 
sublist :: "'a list => nat set => 'a list" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

215 
"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))" 
17086  216 

217 
primrec 

34941  218 
splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
219 
"splice [] ys = ys" 

220 
 "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))" 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

221 
 {*Warning: simpset does not contain the second eqn but a derived one. *} 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

222 

26771  223 
text{* 
224 
\begin{figure}[htbp] 

225 
\fbox{ 

226 
\begin{tabular}{l} 

27381  227 
@{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\ 
228 
@{lemma "length [a,b,c] = 3" by simp}\\ 

229 
@{lemma "set [a,b,c] = {a,b,c}" by simp}\\ 

230 
@{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\ 

231 
@{lemma "rev [a,b,c] = [c,b,a]" by simp}\\ 

232 
@{lemma "hd [a,b,c,d] = a" by simp}\\ 

233 
@{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\ 

234 
@{lemma "last [a,b,c,d] = d" by simp}\\ 

235 
@{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\ 

236 
@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\ 

237 
@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\ 

238 
@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\ 

239 
@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\ 

240 
@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\ 

241 
@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ 

242 
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ 

243 
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ 

244 
@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\ 

245 
@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\ 

246 
@{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\ 

247 
@{lemma "drop 6 [a,b,c,d] = []" by simp}\\ 

248 
@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\ 

249 
@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\ 

250 
@{lemma "distinct [2,0,1::nat]" by simp}\\ 

251 
@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\ 

34978
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

252 
@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ 
35295  253 
@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\ 
27381  254 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  255 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  256 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
257 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

258 
@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\ 

259 
@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\ 

35216  260 
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\ 
261 
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\ 

262 
@{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\ 

27381  263 
@{lemma "listsum [1,2,3::nat] = 6" by simp} 
26771  264 
\end{tabular}} 
265 
\caption{Characteristic examples} 

266 
\label{fig:Characteristic} 

267 
\end{figure} 

29927  268 
Figure~\ref{fig:Characteristic} shows characteristic examples 
26771  269 
that should give an intuitive understanding of the above functions. 
270 
*} 

271 

24616  272 
text{* The following simple sort functions are intended for proofs, 
273 
not for efficient implementations. *} 

274 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

275 
context linorder 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

276 
begin 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

277 

5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

278 
fun sorted :: "'a list \<Rightarrow> bool" where 
24697  279 
"sorted [] \<longleftrightarrow> True"  
280 
"sorted [x] \<longleftrightarrow> True"  

25062  281 
"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)" 
24697  282 

33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

283 
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

284 
"insort_key f x [] = [x]"  
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

285 
"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))" 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

286 

35195  287 
definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
288 
"sort_key f xs = foldr (insort_key f) xs []" 

33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

289 

603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

290 
abbreviation "sort \<equiv> sort_key (\<lambda>x. x)" 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

291 
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)" 
24616  292 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

293 
end 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

294 

24616  295 

23388  296 
subsubsection {* List comprehension *} 
23192  297 

24349  298 
text{* Input syntax for Haskelllike list comprehension notation. 
299 
Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"}, 

300 
the list of all pairs of distinct elements from @{text xs} and @{text ys}. 

301 
The syntax is as in Haskell, except that @{text""} becomes a dot 

302 
(like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than 

303 
\verb![e x < xs, ...]!. 

304 

305 
The qualifiers after the dot are 

306 
\begin{description} 

307 
\item[generators] @{text"p \<leftarrow> xs"}, 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

308 
where @{text p} is a pattern and @{text xs} an expression of list type, or 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

309 
\item[guards] @{text"b"}, where @{text b} is a boolean expression. 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

310 
%\item[local bindings] @ {text"let x = e"}. 
24349  311 
\end{description} 
23240  312 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

313 
Just like in Haskell, list comprehension is just a shorthand. To avoid 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

314 
misunderstandings, the translation into desugared form is not reversed 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

315 
upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

316 
optmized to @{term"map (%x. e) xs"}. 
23240  317 

24349  318 
It is easy to write short list comprehensions which stand for complex 
319 
expressions. During proofs, they may become unreadable (and 

320 
mangled). In such cases it can be advisable to introduce separate 

321 
definitions for the list comprehensions in question. *} 

322 

23209  323 
(* 
23240  324 
Proper theorem proving support would be nice. For example, if 
23192  325 
@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"} 
326 
produced something like 

23209  327 
@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}. 
328 
*) 

329 

23240  330 
nonterminals lc_qual lc_quals 
23192  331 

332 
syntax 

23240  333 
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __") 
24349  334 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ < _") 
23240  335 
"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_") 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

336 
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*) 
23240  337 
"_lc_end" :: "lc_quals" ("]") 
338 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 

24349  339 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  340 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

341 
(* These are easier than ML code but cannot express the optimized 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

342 
translation of [e. p<xs] 
23192  343 
translations 
24349  344 
"[e. p<xs]" => "concat(map (_lc_abs p [e]) xs)" 
23240  345 
"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" 
24349  346 
=> "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)" 
23240  347 
"[e. P]" => "if P then [e] else []" 
348 
"_listcompr e (_lc_test P) (_lc_quals Q Qs)" 

349 
=> "if P then (_listcompr e Q Qs) else []" 

24349  350 
"_listcompr e (_lc_let b) (_lc_quals Q Qs)" 
351 
=> "_Let b (_listcompr e Q Qs)" 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

352 
*) 
23240  353 

23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

354 
syntax (xsymbols) 
24349  355 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

356 
syntax (HTML output) 
24349  357 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
358 

359 
parse_translation (advanced) {* 

360 
let 

35256  361 
val NilC = Syntax.const @{const_syntax Nil}; 
362 
val ConsC = Syntax.const @{const_syntax Cons}; 

363 
val mapC = Syntax.const @{const_syntax map}; 

364 
val concatC = Syntax.const @{const_syntax concat}; 

365 
val IfC = Syntax.const @{const_syntax If}; 

35115  366 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

367 
fun singl x = ConsC $ x $ NilC; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

368 

35115  369 
fun pat_tr ctxt p e opti = (* %x. case x of p => e  _ => [] *) 
24349  370 
let 
29281  371 
val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT); 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

372 
val e = if opti then singl e else e; 
35115  373 
val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; 
35256  374 
val case2 = 
375 
Syntax.const @{syntax_const "_case1"} $ 

376 
Syntax.const @{const_syntax dummy_pattern} $ NilC; 

35115  377 
val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; 
378 
val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs]; 

24349  379 
in lambda x ft end; 
380 

35256  381 
fun abs_tr ctxt (p as Free (s, T)) e opti = 
35115  382 
let 
383 
val thy = ProofContext.theory_of ctxt; 

384 
val s' = Sign.intern_const thy s; 

385 
in 

386 
if Sign.declared_const thy s' 

387 
then (pat_tr ctxt p e opti, false) 

388 
else (lambda p e, true) 

24349  389 
end 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

390 
 abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false); 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

391 

35115  392 
fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] = 
393 
let 

394 
val res = 

395 
(case qs of 

396 
Const (@{syntax_const "_lc_end"}, _) => singl e 

397 
 Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]); 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

398 
in IfC $ b $ res $ NilC end 
35115  399 
 lc_tr ctxt 
400 
[e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, 

401 
Const(@{syntax_const "_lc_end"}, _)] = 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

402 
(case abs_tr ctxt p e true of 
35115  403 
(f, true) => mapC $ f $ es 
404 
 (f, false) => concatC $ (mapC $ f $ es)) 

405 
 lc_tr ctxt 

406 
[e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, 

407 
Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] = 

408 
let val e' = lc_tr ctxt [e, q, qs]; 

409 
in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end; 

410 

411 
in [(@{syntax_const "_listcompr"}, lc_tr)] end 

24349  412 
*} 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

413 

23240  414 
term "[(x,y,z). b]" 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

415 
term "[(x,y,z). x\<leftarrow>xs]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

416 
term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

417 
term "[(x,y,z). x<a, x>b]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

418 
term "[(x,y,z). x\<leftarrow>xs, x>b]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

419 
term "[(x,y,z). x<a, x\<leftarrow>xs]" 
24349  420 
term "[(x,y). Cons True x \<leftarrow> xs]" 
421 
term "[(x,y,z). Cons x [] \<leftarrow> xs]" 

23240  422 
term "[(x,y,z). x<a, x>b, x=d]" 
423 
term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]" 

424 
term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]" 

425 
term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]" 

426 
term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]" 

427 
term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]" 

428 
term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]" 

429 
term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]" 

35115  430 
(* 
24349  431 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  432 
*) 
433 

35115  434 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

435 
subsubsection {* @{const Nil} and @{const Cons} *} 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

436 

580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

437 
lemma not_Cons_self [simp]: 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

438 
"xs \<noteq> x # xs" 
13145  439 
by (induct xs) auto 
13114  440 

13142  441 
lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] 
13114  442 

13142  443 
lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)" 
13145  444 
by (induct xs) auto 
13114  445 

13142  446 
lemma length_induct: 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

447 
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 
17589  448 
by (rule measure_induct [of length]) iprover 
13114  449 

450 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

451 
subsubsection {* @{const length} *} 
13114  452 

13142  453 
text {* 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

454 
Needs to come before @{text "@"} because of theorem @{text 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

455 
append_eq_append_conv}. 
13142  456 
*} 
13114  457 

13142  458 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  459 
by (induct xs) auto 
13114  460 

13142  461 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  462 
by (induct xs) auto 
13114  463 

13142  464 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  465 
by (induct xs) auto 
13114  466 

13142  467 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  468 
by (cases xs) auto 
13114  469 

13142  470 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  471 
by (induct xs) auto 
13114  472 

13142  473 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  474 
by (induct xs) auto 
13114  475 

23479  476 
lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0" 
477 
by auto 

478 

13114  479 
lemma length_Suc_conv: 
13145  480 
"(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" 
481 
by (induct xs) auto 

13142  482 

14025  483 
lemma Suc_length_conv: 
484 
"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" 

14208  485 
apply (induct xs, simp, simp) 
14025  486 
apply blast 
487 
done 

488 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

489 
lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

490 
by (induct xs) auto 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

491 

26442
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

492 
lemma list_induct2 [consumes 1, case_names Nil Cons]: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

493 
"length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow> 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

494 
(\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys)) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

495 
\<Longrightarrow> P xs ys" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

496 
proof (induct xs arbitrary: ys) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

497 
case Nil then show ?case by simp 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

498 
next 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

499 
case (Cons x xs ys) then show ?case by (cases ys) simp_all 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

500 
qed 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

501 

57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

502 
lemma list_induct3 [consumes 2, case_names Nil Cons]: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

503 
"length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow> 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

504 
(\<And>x xs y ys z zs. length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P xs ys zs \<Longrightarrow> P (x#xs) (y#ys) (z#zs)) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

505 
\<Longrightarrow> P xs ys zs" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

506 
proof (induct xs arbitrary: ys zs) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

507 
case Nil then show ?case by simp 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

508 
next 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

509 
case (Cons x xs ys zs) then show ?case by (cases ys, simp_all) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

510 
(cases zs, simp_all) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

511 
qed 
13114  512 

22493
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

513 
lemma list_induct2': 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

514 
"\<lbrakk> P [] []; 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

515 
\<And>x xs. P (x#xs) []; 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

516 
\<And>y ys. P [] (y#ys); 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

517 
\<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk> 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

518 
\<Longrightarrow> P xs ys" 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

519 
by (induct xs arbitrary: ys) (case_tac x, auto)+ 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

520 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

521 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  522 
by (rule Eq_FalseI) auto 
24037  523 

524 
simproc_setup list_neq ("(xs::'a list) = ys") = {* 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

525 
(* 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

526 
Reduces xs=ys to False if xs and ys cannot be of the same length. 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

527 
This is the case if the atomic sublists of one are a submultiset 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

528 
of those of the other list and there are fewer Cons's in one than the other. 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

529 
*) 
24037  530 

531 
let 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

532 

29856  533 
fun len (Const(@{const_name Nil},_)) acc = acc 
534 
 len (Const(@{const_name Cons},_) $ _ $ xs) (ts,n) = len xs (ts,n+1) 

535 
 len (Const(@{const_name append},_) $ xs $ ys) acc = len xs (len ys acc) 

536 
 len (Const(@{const_name rev},_) $ xs) acc = len xs acc 

537 
 len (Const(@{const_name map},_) $ _ $ xs) acc = len xs acc 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

538 
 len t (ts,n) = (t::ts,n); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

539 

24037  540 
fun list_neq _ ss ct = 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

541 
let 
24037  542 
val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct; 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

543 
val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

544 
fun prove_neq() = 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

545 
let 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

546 
val Type(_,listT::_) = eqT; 
22994  547 
val size = HOLogic.size_const listT; 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

548 
val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

549 
val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

550 
val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len 
22633  551 
(K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1)); 
552 
in SOME (thm RS @{thm neq_if_length_neq}) end 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

553 
in 
23214  554 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
555 
n < m andalso submultiset (op aconv) (rs,ls) 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

556 
then prove_neq() else NONE 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

557 
end; 
24037  558 
in list_neq end; 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

559 
*} 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

560 

cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

561 

15392  562 
subsubsection {* @{text "@"}  append *} 
13114  563 

13142  564 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  565 
by (induct xs) auto 
13114  566 

13142  567 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  568 
by (induct xs) auto 
3507  569 

13142  570 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  571 
by (induct xs) auto 
13114  572 

13142  573 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  574 
by (induct xs) auto 
13114  575 

13142  576 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  577 
by (induct xs) auto 
13114  578 

13142  579 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  580 
by (induct xs) auto 
13114  581 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

582 
lemma append_eq_append_conv [simp, noatp]: 
24526  583 
"length xs = length ys \<or> length us = length vs 
13883
0451e0fb3f22
Restructured some proofs in order to get rid of rule_format attribute.
berghofe
parents:
13863
diff
changeset

584 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  585 
apply (induct xs arbitrary: ys) 
14208  586 
apply (case_tac ys, simp, force) 
587 
apply (case_tac ys, force, simp) 

13145  588 
done 
13142  589 

24526  590 
lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) = 
591 
(EX us. xs = zs @ us & us @ ys = ts  xs @ us = zs & ys = us@ ts)" 

592 
apply (induct xs arbitrary: ys zs ts) 

14495  593 
apply fastsimp 
594 
apply(case_tac zs) 

595 
apply simp 

596 
apply fastsimp 

597 
done 

598 

34910
b23bd3ee4813
same_append_eq / append_same_eq are now used for simplifying induction rules.
berghofe
parents:
34064
diff
changeset

599 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  600 
by simp 
13142  601 

602 
lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)" 

13145  603 
by simp 
13114  604 

34910
b23bd3ee4813
same_append_eq / append_same_eq are now used for simplifying induction rules.
berghofe
parents:
34064
diff
changeset

605 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  606 
by simp 
13114  607 

13142  608 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  609 
using append_same_eq [of _ _ "[]"] by auto 
3507  610 

13142  611 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  612 
using append_same_eq [of "[]"] by auto 
13114  613 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24219
diff
changeset

614 
lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
13145  615 
by (induct xs) auto 
13114  616 

13142  617 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  618 
by (induct xs) auto 
13114  619 

13142  620 
lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs" 
13145  621 
by (simp add: hd_append split: list.split) 
13114  622 

13142  623 
lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys  z#zs => zs @ ys)" 
13145  624 
by (simp split: list.split) 
13114  625 

13142  626 
lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys" 
13145  627 
by (simp add: tl_append split: list.split) 
13114  628 

629 

14300  630 
lemma Cons_eq_append_conv: "x#xs = ys@zs = 
631 
(ys = [] & x#xs = zs  (EX ys'. x#ys' = ys & xs = ys'@zs))" 

632 
by(cases ys) auto 

633 

15281  634 
lemma append_eq_Cons_conv: "(ys@zs = x#xs) = 
635 
(ys = [] & zs = x#xs  (EX ys'. ys = x#ys' & ys'@zs = xs))" 

636 
by(cases ys) auto 

637 

14300  638 

13142  639 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  640 

641 
lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys" 

13145  642 
by simp 
13114  643 

13142  644 
lemma Cons_eq_appendI: 
13145  645 
"[ x # xs1 = ys; xs = xs1 @ zs ] ==> x # xs = ys @ zs" 
646 
by (drule sym) simp 

13114  647 

13142  648 
lemma append_eq_appendI: 
13145  649 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
650 
by (drule sym) simp 

13114  651 

652 

13142  653 
text {* 
13145  654 
Simplification procedure for all list equalities. 
655 
Currently only tries to rearrange @{text "@"} to see if 

656 
 both lists end in a singleton list, 

657 
 or both lists end in the same list. 

13142  658 
*} 
659 

26480  660 
ML {* 
3507  661 
local 
662 

29856  663 
fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) = 
664 
(case xs of Const(@{const_name Nil},_) => cons  _ => last xs) 

665 
 last (Const(@{const_name append},_) $ _ $ ys) = last ys 

13462  666 
 last t = t; 
13114  667 

29856  668 
fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true 
13462  669 
 list1 _ = false; 
13114  670 

29856  671 
fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) = 
672 
(case xs of Const(@{const_name Nil},_) => xs  _ => cons $ butlast xs) 

673 
 butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys 

674 
 butlast xs = Const(@{const_name Nil},fastype_of xs); 

13114  675 

22633  676 
val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc}, 
677 
@{thm append_Nil}, @{thm append_Cons}]; 

16973  678 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19890
diff
changeset

679 
fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 
13462  680 
let 
681 
val lastl = last lhs and lastr = last rhs; 

682 
fun rearr conv = 

683 
let 

684 
val lhs1 = butlast lhs and rhs1 = butlast rhs; 

685 
val Type(_,listT::_) = eqT 

686 
val appT = [listT,listT] > listT 

29856  687 
val app = Const(@{const_name append},appT) 
13462  688 
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr) 
13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset

689 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2)); 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19890
diff
changeset

690 
val thm = Goal.prove (Simplifier.the_context ss) [] [] eq 
17877
67d5ab1cb0d8
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
wenzelm
parents:
17830
diff
changeset

691 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  692 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  693 

13462  694 
in 
22633  695 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
696 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  697 
else NONE 
13462  698 
end; 
699 

13114  700 
in 
13462  701 

702 
val list_eq_simproc = 

32010  703 
Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq); 
13462  704 

13114  705 
end; 
706 

707 
Addsimprocs [list_eq_simproc]; 

708 
*} 

709 

710 

15392  711 
subsubsection {* @{text map} *} 
13114  712 

13142  713 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  714 
by (induct xs) simp_all 
13114  715 

13142  716 
lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)" 
13145  717 
by (rule ext, induct_tac xs) auto 
13114  718 

13142  719 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  720 
by (induct xs) auto 
13114  721 

33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

722 
lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs" 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

723 
by (induct xs) auto 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

724 

35208  725 
lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)" 
726 
apply(rule ext) 

727 
apply(simp) 

728 
done 

729 

13142  730 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  731 
by (induct xs) auto 
13114  732 

13737  733 
lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)" 
734 
by (induct xs) auto 

735 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19623
diff
changeset

736 
lemma map_cong [fundef_cong, recdef_cong]: 
13145  737 
"xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys" 
738 
 {* a congruence rule for @{text map} *} 

13737  739 
by simp 
13114  740 

13142  741 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  742 
by (cases xs) auto 
13114  743 

13142  744 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  745 
by (cases xs) auto 
13114  746 

18447  747 
lemma map_eq_Cons_conv: 
14025  748 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  749 
by (cases xs) auto 
13114  750 

18447  751 
lemma Cons_eq_map_conv: 
14025  752 
"(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)" 
753 
by (cases ys) auto 

754 

18447  755 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
756 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

757 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

758 

14111  759 
lemma ex_map_conv: 
760 
"(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)" 

18447  761 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  762 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

763 
lemma map_eq_imp_length_eq: 
35510  764 
assumes "map f xs = map g ys" 
26734  765 
shows "length xs = length ys" 
766 
using assms proof (induct ys arbitrary: xs) 

767 
case Nil then show ?case by simp 

768 
next 

769 
case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto 

35510  770 
from Cons xs have "map f zs = map g ys" by simp 
26734  771 
moreover with Cons have "length zs = length ys" by blast 
772 
with xs show ?case by simp 

773 
qed 

774 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

775 
lemma map_inj_on: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

776 
"[ map f xs = map f ys; inj_on f (set xs Un set ys) ] 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

777 
==> xs = ys" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

778 
apply(frule map_eq_imp_length_eq) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

779 
apply(rotate_tac 1) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

780 
apply(induct rule:list_induct2) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

781 
apply simp 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

782 
apply(simp) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

783 
apply (blast intro:sym) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

784 
done 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

785 

78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

786 
lemma inj_on_map_eq_map: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

787 
"inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

788 
by(blast dest:map_inj_on) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

789 

13114  790 
lemma map_injective: 
24526  791 
"map f xs = map f ys ==> inj f ==> xs = ys" 
792 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  793 

14339  794 
lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)" 
795 
by(blast dest:map_injective) 

796 

13114  797 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  798 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  799 

800 
lemma inj_mapD: "inj (map f) ==> inj f" 

14208  801 
apply (unfold inj_on_def, clarify) 
13145  802 
apply (erule_tac x = "[x]" in ballE) 
14208  803 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  804 
apply blast 
805 
done 

13114  806 

14339  807 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  808 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  809 

15303  810 
lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A" 
811 
apply(rule inj_onI) 

812 
apply(erule map_inj_on) 

813 
apply(blast intro:inj_onI dest:inj_onD) 

814 
done 

815 

14343  816 
lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs" 
817 
by (induct xs, auto) 

13114  818 

14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

819 
lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs" 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

820 
by (induct xs) auto 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

821 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

822 
lemma map_fst_zip[simp]: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

823 
"length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

824 
by (induct rule:list_induct2, simp_all) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

825 

78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

826 
lemma map_snd_zip[simp]: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

827 
"length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

828 
by (induct rule:list_induct2, simp_all) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

829 

78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

830 

15392  831 
subsubsection {* @{text rev} *} 
13114  832 

13142  833 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  834 
by (induct xs) auto 
13114  835 

13142  836 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  837 
by (induct xs) auto 
13114  838 

15870  839 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
840 
by auto 

841 

13142  842 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  843 
by (induct xs) auto 
13114  844 

13142  845 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  846 
by (induct xs) auto 
13114  847 

15870  848 
lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])" 
849 
by (cases xs) auto 

850 

851 
lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])" 

852 
by (cases xs) auto 

853 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

854 
lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)" 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

855 
apply (induct xs arbitrary: ys, force) 
14208  856 
apply (case_tac ys, simp, force) 
13145  857 
done 
13114  858 

15439  859 
lemma inj_on_rev[iff]: "inj_on rev A" 
860 
by(simp add:inj_on_def) 

861 

13366  862 
lemma rev_induct [case_names Nil snoc]: 
863 
"[ P []; !!x xs. P xs ==> P (xs @ [x]) ] ==> P xs" 

15489
d136af442665
Replaced application of subst by simplesubst in proof of rev_induct
berghofe
parents:
15439
diff
changeset

864 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  865 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
866 
done 

13114  867 

13366  868 
lemma rev_exhaust [case_names Nil snoc]: 
869 
"(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P" 

13145  870 
by (induct xs rule: rev_induct) auto 
13114  871 

13366  872 
lemmas rev_cases = rev_exhaust 
873 

18423  874 
lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])" 
875 
by(rule rev_cases[of xs]) auto 

876 

13114  877 

15392  878 
subsubsection {* @{text set} *} 
13114  879 

13142  880 
lemma finite_set [iff]: "finite (set xs)" 
13145  881 
by (induct xs) auto 
13114  882 

13142  883 
lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)" 
13145  884 
by (induct xs) auto 
13114  885 

17830  886 
lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs" 
887 
by(cases xs) auto 

14099  888 

13142  889 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  890 
by auto 
13114  891 

14099  892 
lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs" 
893 
by auto 

894 

13142  895 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  896 
by (induct xs) auto 
13114  897 

15245  898 
lemma set_empty2[iff]: "({} = set xs) = (xs = [])" 
899 
by(induct xs) auto 

900 

13142  901 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  902 
by (induct xs) auto 
13114  903 

13142  904 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  905 
by (induct xs) auto 
13114  906 

13142  907 
lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}" 
13145  908 
by (induct xs) auto 
13114  909 

32417  910 
lemma set_upt [simp]: "set[i..<j] = {i..<j}" 
911 
by (induct j) (simp_all add: atLeastLessThanSuc) 

13114  912 

13142  913 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

914 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  915 
proof (induct xs) 
26073  916 
case Nil thus ?case by simp 
917 
next 

918 
case Cons thus ?case by (auto intro: Cons_eq_appendI) 

919 
qed 

920 

26734  921 
lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)" 
922 
by (auto elim: split_list) 

26073  923 

924 
lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys" 

925 
proof (induct xs) 

926 
case Nil thus ?case by simp 

18049  927 
next 
928 
case (Cons a xs) 

929 
show ?case 

930 
proof cases 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

931 
assume "x = a" thus ?case using Cons by fastsimp 
18049  932 
next 
26073  933 
assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI) 
934 
qed 

935 
qed 

936 

937 
lemma in_set_conv_decomp_first: 

938 
"(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)" 

26734  939 
by (auto dest!: split_list_first) 
26073  940 

941 
lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs" 

942 
proof (induct xs rule:rev_induct) 

943 
case Nil thus ?case by simp 

944 
next 

945 
case (snoc a xs) 

946 
show ?case 

947 
proof cases 

948 
assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2) 

949 
next 

950 
assume "x \<noteq> a" thus ?case using snoc by fastsimp 

18049  951 
qed 
952 
qed 

953 

26073  954 
lemma in_set_conv_decomp_last: 
955 
"(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)" 

26734  956 
by (auto dest!: split_list_last) 
26073  957 

958 
lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x" 

959 
proof (induct xs) 

960 
case Nil thus ?case by simp 

961 
next 

962 
case Cons thus ?case 

963 
by(simp add:Bex_def)(metis append_Cons append.simps(1)) 

964 
qed 

965 

966 
lemma split_list_propE: 

26734  967 
assumes "\<exists>x \<in> set xs. P x" 
968 
obtains ys x zs where "xs = ys @ x # zs" and "P x" 

969 
using split_list_prop [OF assms] by blast 

26073  970 

971 
lemma split_list_first_prop: 

972 
"\<exists>x \<in> set xs. P x \<Longrightarrow> 

973 
\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)" 

26734  974 
proof (induct xs) 
26073  975 
case Nil thus ?case by simp 
976 
next 

977 
case (Cons x xs) 

978 
show ?case 

979 
proof cases 

980 
assume "P x" 

26734  981 
thus ?thesis by simp 
982 
(metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 

26073  983 
next 
984 
assume "\<not> P x" 

985 
hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp 

986 
thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD) 

987 
qed 

988 
qed 

989 

990 
lemma split_list_first_propE: 

26734  991 
assumes "\<exists>x \<in> set xs. P x" 
992 
obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y" 

993 
using split_list_first_prop [OF assms] by blast 

26073  994 

995 
lemma split_list_first_prop_iff: 

996 
"(\<exists>x \<in> set xs. P x) \<longleftrightarrow> 

997 
(\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))" 

26734  998 
by (rule, erule split_list_first_prop) auto 
26073  999 

1000 
lemma split_list_last_prop: 

1001 
"\<exists>x \<in> set xs. P x \<Longrightarrow> 

1002 
\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)" 

1003 
proof(induct xs rule:rev_induct) 

1004 
case Nil thus ?case by simp 

1005 
next 

1006 
case (snoc x xs) 

1007 
show ?case 

1008 
proof cases 

1009 
assume "P x" thus ?thesis by (metis emptyE set_empty) 

1010 
next 

1011 
assume "\<not> P x" 

1012 
hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp 

1013 
thus ?thesis using `\<not> P x` snoc(1) by fastsimp 

1014 
qed 

1015 
qed 

1016 

1017 
lemma split_list_last_propE: 

26734  1018 
assumes "\<exists>x \<in> set xs. P x" 
1019 
obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z" 

1020 
using split_list_last_prop [OF assms] by blast 

26073  1021 

1022 
lemma split_list_last_prop_iff: 

1023 
"(\<exists>x \<in> set xs. P x) \<longleftrightarrow> 

1024 
(\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))" 

26734  1025 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1026 

1027 
lemma finite_list: "finite A ==> EX xs. set xs = A" 

26734  1028 
by (erule finite_induct) 
1029 
(auto simp add: set.simps(2) [symmetric] simp del: set.simps(2)) 

13508  1030 

14388  1031 
lemma card_length: "card (set xs) \<le> length xs" 
1032 
by (induct xs) (auto simp add: card_insert_if) 

13114  1033 

26442
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1034 
lemma set_minus_filter_out: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1035 
"set xs  {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1036 
by (induct xs) auto 
15168  1037 

35115  1038 

15392  1039 
subsubsection {* @{text filter} *} 
13114  1040 

13142  1041 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1042 
by (induct xs) auto 
13114  1043 

15305  1044 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1045 
by (induct xs) simp_all 

1046 

13142  1047 
lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs" 
13145  1048 
by (induct xs) auto 
13114  1049 

16998  1050 
lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs" 
1051 
by (induct xs) (auto simp add: le_SucI) 

1052 

18423  1053 
lemma sum_length_filter_compl: 
1054 
"length(filter P xs) + length(filter (%x. ~P x) xs) = length xs" 

1055 
by(induct xs) simp_all 

1056 

13142  1057 
lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs" 
13145  1058 
by (induct xs) auto 
13114  1059 

13142  1060 
lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []" 
13145  1061 
by (induct xs) auto 
13114  1062 

16998  1063 
lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
24349  1064 
by (induct xs) simp_all 
16998  1065 

1066 
lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)" 

1067 
apply (induct xs) 

1068 
apply auto 

1069 
apply(cut_tac P=P and xs=xs in length_filter_le) 

1070 
apply simp 

1071 
done 

13114  1072 

16965  1073 
lemma filter_map: 
1074 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1075 
by (induct xs) simp_all 

1076 

1077 
lemma length_filter_map[simp]: 

1078 
"length (filter P (map f xs)) = length(filter (P o f) xs)" 

1079 
by (simp add:filter_map) 

1080 

13142  1081 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1082 
by auto 
13114  1083 

15246  1084 
lemma length_filter_less: 
1085 
"\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs" 

1086 
proof (induct xs) 

1087 
case Nil thus ?case by simp 

1088 
next 

1089 
case (Cons x xs) thus ?case 

1090 
apply (auto split:split_if_asm) 

1091 
using length_filter_le[of P xs] apply arith 

1092 
done 

1093 
qed 

13114  1094 

15281  1095 
lemma length_filter_conv_card: 
1096 
"length(filter p xs) = card{i. i < length xs & p(xs!i)}" 

1097 
proof (induct xs) 

1098 
case Nil thus ?case by simp 

1099 
next 

1100 
case (Cons x xs) 

1101 
let ?S = "{i. i < length xs & p(xs!i)}" 

1102 
have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite) 

1103 
show ?case (is "?l = card ?S'") 

1104 
proof (cases) 

1105 
assume "p x" 

1106 
hence eq: "?S' = insert 0 (Suc ` ?S)" 

25162  1107 
by(auto simp: image_def split:nat.split dest:gr0_implies_Suc) 
15281  1108 
have "length (filter p (x # xs)) = Suc(card ?S)" 
23388  1109 
using Cons `p x` by simp 
15281  1110 
also have "\<dots> = Suc(card(Suc ` ?S))" using fin 
1111 
by (simp add: card_image inj_Suc) 

1112 
also have "\<dots> = card ?S'" using eq fin 

1113 
by (simp add:card_insert_if) (simp add:image_def) 

1114 
finally show ?thesis . 

1115 
next 

1116 
assume "\<not> p x" 

1117 
hence eq: "?S' = Suc ` ?S" 

25162  1118 
by(auto simp add: image_def split:nat.split elim:lessE) 
15281  1119 
have "length (filter p (x # xs)) = card ?S" 
23388  1120 
using Cons `\<not> p x` by simp 
15281  1121 
also have "\<dots> = card(Suc ` ?S)" using fin 
1122 
by (simp add: card_image inj_Suc) 

1123 
also have "\<dots> = card ?S'" using eq fin 

1124 
by (simp add:card_insert_if) 

1125 
finally show ?thesis . 

1126 
qed 

1127 
qed 

1128 

17629  1129 
lemma Cons_eq_filterD: 
1130 
"x#xs = filter P ys \<Longrightarrow> 

1131 
\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs" 

19585  1132 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1133 
proof(induct ys) 
1134 
case Nil thus ?case by simp 

1135 
next 

1136 
case (Cons y ys) 

1137 
show ?case (is "\<exists>x. ?Q x") 

1138 
proof cases 

1139 
assume Py: "P y" 

1140 
show ?thesis 

1141 
proof cases 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1142 
assume "x = y" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1143 
with Py Cons.prems have "?Q []" by simp 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1144 
then show ?thesis .. 
17629  1145 
next 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1146 
assume "x \<noteq> y" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1147 
with Py Cons.prems show ?thesis by simp 
17629  1148 
qed 
1149 
next 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1150 
assume "\<not> P y" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1151 
with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1152 
then have "?Q (y#us)" by simp 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1153 
then show ?thesis .. 
17629  1154 
qed 
1155 
qed 

1156 

1157 
lemma filter_eq_ConsD: 

1158 
"filter P ys = x#xs \<Longrightarrow> 

1159 
\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs" 

1160 
by(rule Cons_eq_filterD) simp 

1161 

1162 
lemma filter_eq_Cons_iff: 

1163 
"(filter P ys = x#xs) = 

1164 
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)" 

1165 
by(auto dest:filter_eq_ConsD) 

1166 

1167 
lemma Cons_eq_filter_iff: 

1168 
"(x#xs = filter P ys) = 

1169 
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)" 

1170 
by(auto dest:Cons_eq_filterD) 

1171 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19623
diff
changeset

1172 
lemma filter_cong[fundef_cong, recdef_cong]: 
17501  1173 
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys" 
1174 
apply simp 

1175 
apply(erule thin_rl) 

1176 
by (induct ys) simp_all 

1177 

15281  1178 

26442
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1179 
subsubsection {* List partitioning *} 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1180 

57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1181 
primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1182 
"partition P [] = ([], [])" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1183 
 "partition P (x # xs) = 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1184 
(let (yes, no) = partition P xs 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1185 
in if P x then (x # yes, no) else (yes, x # no))" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1186 

57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1187 
lemma partition_filter1: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1188 
"fst (partition P xs) = filter P xs" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1189 
by (induct xs) (auto simp add: Let_def split_def) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1190 

57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1191 
lemma partition_filter2: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1192 
"snd (partition P xs) = filter (Not o P) xs" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1193 
by (induct xs) (auto simp add: Let_def split_def) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1194 

57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1195 
lemma partition_P: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1196 
assumes "partition P xs = (yes, no)" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1197 
shows "(\<forall>p \<in> set yes. P p) \<and> (\<forall>p \<in> set no. \<not> P p)" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1198 
proof  
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1199 
from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1200 
by simp_all 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1201 
then show ?thesis by (simp_all add: partition_filter1 partition_filter2) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1202 
qed 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1203 

57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1204 
lemma partition_set: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1205 
assumes "partition P xs = (yes, no)" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1206 
shows "set yes \<union> set no = set xs" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1207 
proof  
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1208 
from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)" 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1209 
by simp_all 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1210 
then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1211 
qed 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1212 

33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

1213 
lemma partition_filter_conv[simp]: 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

1214 
"partition f xs = (filter f xs,filter (Not o f) xs)" 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

1215 
unfolding partition_filter2[symmetric] 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

1216 
unfolding partition_filter1[symmetric] by simp 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

1217 

603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

1218 
declare partition.simps[simp del] 
26442
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

1219 

35115  1220 

15392  1221 
subsubsection {* @{text concat} *} 
13114  1222 

13142  1223 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1224 
by (induct xs) auto 
13114  1225 

18447  1226 
lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])" 
13145  1227 
by (induct xss) auto 
13114  1228 

18447  1229 
lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])" 
13145  1230 
by (induct xss) auto 
13114  1231 

24308  1232 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1233 
by (induct xs) auto 
13114  1234 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

1235 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1236 
by (induct xs) auto 
1237 

13142  1238 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1239 
by (induct xs) auto 
13114  1240 

13142  1241 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1242 
by (induct xs) auto 
13114  1243 

13142  1244 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1245 
by (induct xs) auto 
13114  1246 

1247 

15392  1248 
subsubsection {* @{text nth} *} 
13114  1249 

29827  1250 
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" 
13145  1251 
by auto 
13114  1252 

29827  1253 
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n" 
13145  1254 
by auto 
13114  1255 

13142  1256 
declare nth.simps [simp del] 
13114  1257 

1258 
lemma nth_append: 

24526  1259 
"(xs @ ys)!n = (if n < length xs then xs!n else ys!(n  length xs))" 
1260 
apply (induct xs arbitrary: n, simp) 

14208  1261 
apply (case_tac n, auto) 
13145  1262 
done 
13114  1263 

14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1264 
lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x" 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1265 
by (induct xs) auto 
14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1266 

4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1267 
lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n" 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1268 
by (induct xs) auto 
14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1269 

24526  1270 
lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)" 
1271 
apply (induct xs arbitrary: n, simp) 

14208  1272 
apply (case_tac n, auto) 
13145  1273 
done 
13114  1274 

18423  1275 
lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0" 
1276 
by(cases xs) simp_all 

1277 

18049  1278 

1279 
lemma list_eq_iff_nth_eq: 

24526  1280 
"(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))" 
1281 
apply(induct xs arbitrary: ys) 

24632  1282 
apply force 
18049  1283 
apply(case_tac ys) 
1284 
apply simp 

1285 
apply(simp add:nth_Cons split:nat.split)apply blast 

1286 
done 

1287 

13142  1288 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  1289 
apply (induct xs, simp, simp) 
13145  1290 
apply safe 
24632  1291 
apply (metis nat_case_0 nth.simps zero_less_Suc) 
1292 
apply (metis less_Suc_eq_0_disj nth_Cons_Suc) 

14208  1293 
apply (case_tac i, simp) 
24632  1294 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1295 
done 
13114  1296 

17501  1297 
lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)" 
1298 
by(auto simp:set_conv_nth) 

1299 

13145  1300 
lemma list_ball_nth: "[ n < length xs; !x : set xs. P x] ==> P(xs!n)" 
1301 
by (auto simp add: set_conv_nth) 

13114  1302 

13142  1303 
lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs" 
13145  1304 
by (auto simp add: set_conv_nth) 
13114  1305 

1306 
lemma all_nth_imp_all_set: 

13145  1307 
"[ !i < length xs. P(xs!i); x : set xs] ==> P x" 
1308 
by (auto simp add: set_conv_nth) 

13114  1309 

1310 
lemma all_set_conv_all_nth: 

13145  1311 
"(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs > P (xs ! i))" 
1312 
by (auto simp add: set_conv_nth) 

13114  1313 

25296  1314 
lemma rev_nth: 
1315 
"n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs  Suc n)" 

1316 
proof (induct xs arbitrary: n) 

1317 
case Nil thus ?case by simp 

1318 
next 

1319 
case (Cons x xs) 

1320 
hence n: "n < Suc (length xs)" by simp 

1321 
moreover 

1322 
{ assume "n < length xs" 

1323 
with n obtain n' where "length xs  n = Suc n'" 

1324 
by (cases "length xs  n", auto) 

1325 
moreover 

1326 
then have "length xs  Suc n = n'" by simp 

1327 
ultimately 

1328 
have "xs ! (length xs  Suc n) = (x # xs) ! (length xs  n)" by simp 

1329 
} 

1330 
ultimately 

1331 
show ?case by (clarsimp simp add: Cons nth_append) 

1332 
qed 

13114  1333 

31159  1334 
lemma Skolem_list_nth: 
1335 
"(ALL i<k. EX x. P i x) = (EX xs. size xs = k & (ALL i<k. P i (xs!i)))" 

1336 
(is "_ = (EX xs. ?P k xs)") 

1337 
proof(induct k) 

1338 
case 0 show ?case by simp 

1339 
next 

1340 
case (Suc k) 

1341 
show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)") 

1342 
proof 

1343 
assume "?R" thus "?L" using Suc by auto 
