author  haftmann 
Sat, 16 Jan 2010 17:15:28 +0100  
changeset 34941  156925dd67af 
parent 34886  873c31d9f10d 
child 34942  d62eddd9e253 
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 *} 

18 
"@list" :: "args => 'a list" ("[(_)]") 

19 

20 
translations 

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

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

23 

15392  24 
subsection{*Basic list processing functions*} 
15302  25 

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

28 
"hd (x # xs) = x" 

29 

30 
primrec 

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

32 
"tl [] = []" 

33 
 "tl (x # xs) = xs" 

34 

35 
primrec 

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

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

38 

39 
primrec 

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

41 
"butlast []= []" 

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

43 

44 
primrec 

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

46 
"set [] = {}" 

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

48 

49 
primrec 

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

51 
"map f [] = []" 

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

53 

54 
primrec 

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

56 
append_Nil:"[] @ ys = ys" 

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

58 

59 
primrec 

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

61 
"rev [] = []" 

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

63 

64 
primrec 

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

66 
"filter P [] = []" 

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

68 

69 
syntax 

70 
 {* Special syntax for filter *} 

71 
"@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<_./ _])") 

72 

73 
translations 

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

75 

76 
syntax (xsymbols) 

77 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 

78 
syntax (HTML output) 

79 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 

80 

81 
primrec 

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

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

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

85 

86 
primrec 

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

88 
"foldr f [] a = a" 

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

90 

91 
primrec 

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

93 
"concat [] = []" 

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

95 

96 
primrec (in monoid_add) 

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

98 
"listsum [] = 0" 

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

100 

101 
primrec 

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

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

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

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

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

107 

108 
primrec 

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

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

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

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

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

114 

115 
primrec 

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

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

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

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

120 

121 
primrec 

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

123 
"list_update [] i v = []" 

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

923  125 

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

127 

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

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

132 
"_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

133 

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

138 
primrec 

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

140 
"takeWhile P [] = []" 

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

142 

143 
primrec 

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

145 
"dropWhile P [] = []" 

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

147 

148 
primrec 

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

150 
"zip xs [] = []" 

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

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

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

154 

155 
primrec 

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

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

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

159 

160 
primrec 

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

162 
"distinct [] \<longleftrightarrow> True" 

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

164 

165 
primrec 

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

167 
"remdups [] = []" 

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

169 

170 
primrec 

171 
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

172 
"remove1 x [] = []" 

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

174 

175 
primrec 

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

177 
"removeAll x [] = []" 

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

179 

180 
primrec 

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

182 
replicate_0: "replicate 0 x = []" 

183 
 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

184 

13142  185 
text {* 
14589  186 
Function @{text size} is overloaded for all datatypes. Users may 
13366  187 
refer to the list version as @{text length}. *} 
13142  188 

19363  189 
abbreviation 
34941  190 
length :: "'a list \<Rightarrow> nat" where 
191 
"length \<equiv> size" 

15307  192 

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

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

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

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

196 

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

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

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

200 

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

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

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

204 
(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

205 

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

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

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

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

210 
primrec 

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

213 
 "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

214 
 {*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

215 

26771  216 
text{* 
217 
\begin{figure}[htbp] 

218 
\fbox{ 

219 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

27693  246 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  247 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
248 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

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

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

251 
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\ 

252 
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\ 

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

254 
@{lemma "listsum [1,2,3::nat] = 6" by simp} 

26771  255 
\end{tabular}} 
256 
\caption{Characteristic examples} 

257 
\label{fig:Characteristic} 

258 
\end{figure} 

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

262 

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

265 

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

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

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

268 

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

269 
fun sorted :: "'a list \<Rightarrow> bool" where 
24697  270 
"sorted [] \<longleftrightarrow> True"  
271 
"sorted [x] \<longleftrightarrow> True"  

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

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

274 
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

275 
"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

276 
"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

277 

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

278 
primrec sort_key :: "('b \<Rightarrow> 'a) \<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

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

280 
"sort_key f (x#xs) = insort_key f x (sort_key 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

281 

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

282 
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

283 
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)" 
24616  284 

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

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

286 

24616  287 

23388  288 
subsubsection {* List comprehension *} 
23192  289 

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

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

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

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

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

296 

297 
The qualifiers after the dot are 

298 
\begin{description} 

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

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

300 
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

301 
\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

302 
%\item[local bindings] @ {text"let x = e"}. 
24349  303 
\end{description} 
23240  304 

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

305 
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

306 
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

307 
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

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

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

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

313 
definitions for the list comprehensions in question. *} 

314 

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

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

321 

23240  322 
nonterminals lc_qual lc_quals 
23192  323 

324 
syntax 

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

328 
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*) 
23240  329 
"_lc_end" :: "lc_quals" ("]") 
330 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 

24349  331 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  332 

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

333 
(* 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

334 
translation of [e. p<xs] 
23192  335 
translations 
24349  336 
"[e. p<xs]" => "concat(map (_lc_abs p [e]) xs)" 
23240  337 
"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" 
24349  338 
=> "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)" 
23240  339 
"[e. P]" => "if P then [e] else []" 
340 
"_listcompr e (_lc_test P) (_lc_quals Q Qs)" 

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

24349  342 
"_listcompr e (_lc_let b) (_lc_quals Q Qs)" 
343 
=> "_Let b (_listcompr e Q Qs)" 

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

344 
*) 
23240  345 

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

346 
syntax (xsymbols) 
24349  347 
"_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

348 
syntax (HTML output) 
24349  349 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
350 

351 
parse_translation (advanced) {* 

352 
let 

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

353 
val NilC = Syntax.const @{const_name Nil}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

354 
val ConsC = Syntax.const @{const_name Cons}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

355 
val mapC = Syntax.const @{const_name map}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

356 
val concatC = Syntax.const @{const_name concat}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

357 
val IfC = Syntax.const @{const_name If}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

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

359 

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

360 
fun pat_tr ctxt p e opti = (* %x. case x of p => e  _ => [] *) 
24349  361 
let 
29281  362 
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

363 
val e = if opti then singl e else e; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

364 
val case1 = Syntax.const "_case1" $ p $ e; 
24349  365 
val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

366 
$ NilC; 
24349  367 
val cs = Syntax.const "_case2" $ case1 $ case2 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33640
diff
changeset

368 
val ft = Datatype_Case.case_tr false Datatype.info_of_constr 
24349  369 
ctxt [x, cs] 
370 
in lambda x ft end; 

371 

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

372 
fun abs_tr ctxt (p as Free(s,T)) e opti = 
24349  373 
let val thy = ProofContext.theory_of ctxt; 
374 
val s' = Sign.intern_const thy s 

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

375 
in if Sign.declared_const thy s' 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

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

377 
else (lambda p e, true) 
24349  378 
end 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

379 
 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

380 

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

381 
fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] = 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

382 
let val res = case qs of Const("_lc_end",_) => singl e 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

383 
 Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs]; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

384 
in IfC $ b $ res $ NilC end 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

385 
 lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] = 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

386 
(case abs_tr ctxt p e true of 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

387 
(f,true) => mapC $ f $ es 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

388 
 (f, false) => concatC $ (mapC $ f $ es)) 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

389 
 lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] = 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

390 
let val e' = lc_tr ctxt [e,q,qs]; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

391 
in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

392 

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

393 
in [("_listcompr", lc_tr)] end 
24349  394 
*} 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

395 

23240  396 
(* 
397 
term "[(x,y,z). b]" 

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

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

399 
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

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

401 
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

402 
term "[(x,y,z). x<a, x\<leftarrow>xs]" 
24349  403 
term "[(x,y). Cons True x \<leftarrow> xs]" 
404 
term "[(x,y,z). Cons x [] \<leftarrow> xs]" 

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

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

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

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

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

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

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

24349  413 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  414 
*) 
415 

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

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

417 

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

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

419 
"xs \<noteq> x # xs" 
13145  420 
by (induct xs) auto 
13114  421 

13142  422 
lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] 
13114  423 

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

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

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

431 

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

432 
subsubsection {* @{const length} *} 
13114  433 

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

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

436 
append_eq_append_conv}. 
13142  437 
*} 
13114  438 

13142  439 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  440 
by (induct xs) auto 
13114  441 

13142  442 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  443 
by (induct xs) auto 
13114  444 

13142  445 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  446 
by (induct xs) auto 
13114  447 

13142  448 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  449 
by (cases xs) auto 
13114  450 

13142  451 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  452 
by (induct xs) auto 
13114  453 

13142  454 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  455 
by (induct xs) auto 
13114  456 

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

459 

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

13142  463 

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

14208  466 
apply (induct xs, simp, simp) 
14025  467 
apply blast 
468 
done 

469 

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

470 
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

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

472 

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

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

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

475 
(\<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

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

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

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

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

480 
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

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

482 

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

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

484 
"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

485 
(\<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

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

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

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

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

490 
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

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

492 
qed 
13114  493 

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

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

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

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

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

498 
\<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

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

500 
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

501 

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

502 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  503 
by (rule Eq_FalseI) auto 
24037  504 

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

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

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

507 
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

508 
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

509 
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

510 
*) 
24037  511 

512 
let 

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

513 

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

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

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

518 
 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

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

520 

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

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

524 
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

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

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

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

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

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

531 
val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len 
22633  532 
(K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1)); 
533 
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

534 
in 
23214  535 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
536 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

541 

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

542 

15392  543 
subsubsection {* @{text "@"}  append *} 
13114  544 

13142  545 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  546 
by (induct xs) auto 
13114  547 

13142  548 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  549 
by (induct xs) auto 
3507  550 

13142  551 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  552 
by (induct xs) auto 
13114  553 

13142  554 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  555 
by (induct xs) auto 
13114  556 

13142  557 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  558 
by (induct xs) auto 
13114  559 

13142  560 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  561 
by (induct xs) auto 
13114  562 

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

563 
lemma append_eq_append_conv [simp, noatp]: 
24526  564 
"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

565 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  566 
apply (induct xs arbitrary: ys) 
14208  567 
apply (case_tac ys, simp, force) 
568 
apply (case_tac ys, force, simp) 

13145  569 
done 
13142  570 

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

573 
apply (induct xs arbitrary: ys zs ts) 

14495  574 
apply fastsimp 
575 
apply(case_tac zs) 

576 
apply simp 

577 
apply fastsimp 

578 
done 

579 

13142  580 
lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  581 
by simp 
13142  582 

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

13145  584 
by simp 
13114  585 

13142  586 
lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  587 
by simp 
13114  588 

13142  589 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  590 
using append_same_eq [of _ _ "[]"] by auto 
3507  591 

13142  592 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  593 
using append_same_eq [of "[]"] by auto 
13114  594 

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

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

13142  598 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  599 
by (induct xs) auto 
13114  600 

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

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

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

610 

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

613 
by(cases ys) auto 

614 

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

617 
by(cases ys) auto 

618 

14300  619 

13142  620 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  621 

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

13145  623 
by simp 
13114  624 

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

13114  628 

13142  629 
lemma append_eq_appendI: 
13145  630 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
631 
by (drule sym) simp 

13114  632 

633 

13142  634 
text {* 
13145  635 
Simplification procedure for all list equalities. 
636 
Currently only tries to rearrange @{text "@"} to see if 

637 
 both lists end in a singleton list, 

638 
 or both lists end in the same list. 

13142  639 
*} 
640 

26480  641 
ML {* 
3507  642 
local 
643 

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

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

13462  647 
 last t = t; 
13114  648 

29856  649 
fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true 
13462  650 
 list1 _ = false; 
13114  651 

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

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

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

13114  656 

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

16973  659 

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

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

663 
fun rearr conv = 

664 
let 

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

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

667 
val appT = [listT,listT] > listT 

29856  668 
val app = Const(@{const_name append},appT) 
13462  669 
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

670 
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

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

672 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  673 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  674 

13462  675 
in 
22633  676 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
677 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  678 
else NONE 
13462  679 
end; 
680 

13114  681 
in 
13462  682 

683 
val list_eq_simproc = 

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

13114  686 
end; 
687 

688 
Addsimprocs [list_eq_simproc]; 

689 
*} 

690 

691 

15392  692 
subsubsection {* @{text map} *} 
13114  693 

13142  694 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  695 
by (induct xs) simp_all 
13114  696 

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

13142  700 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  701 
by (induct xs) auto 
13114  702 

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

703 
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

704 
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

705 

13142  706 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  707 
by (induct xs) auto 
13114  708 

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

711 

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

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

13737  715 
by simp 
13114  716 

13142  717 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  718 
by (cases xs) auto 
13114  719 

13142  720 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  721 
by (cases xs) auto 
13114  722 

18447  723 
lemma map_eq_Cons_conv: 
14025  724 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  725 
by (cases xs) auto 
13114  726 

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

730 

18447  731 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
732 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

733 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

734 

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

18447  737 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  738 

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

739 
lemma map_eq_imp_length_eq: 
26734  740 
assumes "map f xs = map f ys" 
741 
shows "length xs = length ys" 

742 
using assms proof (induct ys arbitrary: xs) 

743 
case Nil then show ?case by simp 

744 
next 

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

746 
from Cons xs have "map f zs = map f ys" by simp 

747 
moreover with Cons have "length zs = length ys" by blast 

748 
with xs show ?case by simp 

749 
qed 

750 

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

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

752 
"[ 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

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

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

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

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

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

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

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

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

761 

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

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

763 
"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

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

765 

13114  766 
lemma map_injective: 
24526  767 
"map f xs = map f ys ==> inj f ==> xs = ys" 
768 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  769 

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

772 

13114  773 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  774 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  775 

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

14208  777 
apply (unfold inj_on_def, clarify) 
13145  778 
apply (erule_tac x = "[x]" in ballE) 
14208  779 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  780 
apply blast 
781 
done 

13114  782 

14339  783 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  784 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  785 

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

788 
apply(erule map_inj_on) 

789 
apply(blast intro:inj_onI dest:inj_onD) 

790 
done 

791 

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

13114  794 

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

795 
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

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

797 

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

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

799 
"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

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

801 

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

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

803 
"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

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

805 

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

806 

15392  807 
subsubsection {* @{text rev} *} 
13114  808 

13142  809 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  810 
by (induct xs) auto 
13114  811 

13142  812 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  813 
by (induct xs) auto 
13114  814 

15870  815 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
816 
by auto 

817 

13142  818 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  819 
by (induct xs) auto 
13114  820 

13142  821 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  822 
by (induct xs) auto 
13114  823 

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

826 

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

828 
by (cases xs) auto 

829 

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

830 
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

831 
apply (induct xs arbitrary: ys, force) 
14208  832 
apply (case_tac ys, simp, force) 
13145  833 
done 
13114  834 

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

837 

13366  838 
lemma rev_induct [case_names Nil snoc]: 
839 
"[ 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

840 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  841 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
842 
done 

13114  843 

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

13145  846 
by (induct xs rule: rev_induct) auto 
13114  847 

13366  848 
lemmas rev_cases = rev_exhaust 
849 

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

852 

13114  853 

15392  854 
subsubsection {* @{text set} *} 
13114  855 

13142  856 
lemma finite_set [iff]: "finite (set xs)" 
13145  857 
by (induct xs) auto 
13114  858 

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

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

14099  864 

13142  865 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  866 
by auto 
13114  867 

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

870 

13142  871 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  872 
by (induct xs) auto 
13114  873 

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

876 

13142  877 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  878 
by (induct xs) auto 
13114  879 

13142  880 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  881 
by (induct xs) auto 
13114  882 

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

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

13114  888 

13142  889 

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

890 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  891 
proof (induct xs) 
26073  892 
case Nil thus ?case by simp 
893 
next 

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

895 
qed 

896 

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

26073  899 

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

901 
proof (induct xs) 

902 
case Nil thus ?case by simp 

18049  903 
next 
904 
case (Cons a xs) 

905 
show ?case 

906 
proof cases 

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

907 
assume "x = a" thus ?case using Cons by fastsimp 
18049  908 
next 
26073  909 
assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI) 
910 
qed 

911 
qed 

912 

913 
lemma in_set_conv_decomp_first: 

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

26734  915 
by (auto dest!: split_list_first) 
26073  916 

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

918 
proof (induct xs rule:rev_induct) 

919 
case Nil thus ?case by simp 

920 
next 

921 
case (snoc a xs) 

922 
show ?case 

923 
proof cases 

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

925 
next 

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

18049  927 
qed 
928 
qed 

929 

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

26734  932 
by (auto dest!: split_list_last) 
26073  933 

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

935 
proof (induct xs) 

936 
case Nil thus ?case by simp 

937 
next 

938 
case Cons thus ?case 

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

940 
qed 

941 

942 
lemma split_list_propE: 

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

945 
using split_list_prop [OF assms] by blast 

26073  946 

947 
lemma split_list_first_prop: 

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

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

26734  950 
proof (induct xs) 
26073  951 
case Nil thus ?case by simp 
952 
next 

953 
case (Cons x xs) 

954 
show ?case 

955 
proof cases 

956 
assume "P x" 

26734  957 
thus ?thesis by simp 
958 
(metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 

26073  959 
next 
960 
assume "\<not> P x" 

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

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

963 
qed 

964 
qed 

965 

966 
lemma split_list_first_propE: 

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

969 
using split_list_first_prop [OF assms] by blast 

26073  970 

971 
lemma split_list_first_prop_iff: 

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

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

26734  974 
by (rule, erule split_list_first_prop) auto 
26073  975 

976 
lemma split_list_last_prop: 

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

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

979 
proof(induct xs rule:rev_induct) 

980 
case Nil thus ?case by simp 

981 
next 

982 
case (snoc x xs) 

983 
show ?case 

984 
proof cases 

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

986 
next 

987 
assume "\<not> P x" 

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

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

990 
qed 

991 
qed 

992 

993 
lemma split_list_last_propE: 

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

996 
using split_list_last_prop [OF assms] by blast 

26073  997 

998 
lemma split_list_last_prop_iff: 

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

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

26734  1001 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1002 

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

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

13508  1006 

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

13114  1009 

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

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

1011 
"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

1012 
by (induct xs) auto 
15168  1013 

15392  1014 
subsubsection {* @{text filter} *} 
13114  1015 

13142  1016 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1017 
by (induct xs) auto 
13114  1018 

15305  1019 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1020 
by (induct xs) simp_all 

1021 

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

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

1027 

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

1030 
by(induct xs) simp_all 

1031 

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

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

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

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

1042 
apply (induct xs) 

1043 
apply auto 

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

1045 
apply simp 

1046 
done 

13114  1047 

16965  1048 
lemma filter_map: 
1049 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1050 
by (induct xs) simp_all 

1051 

1052 
lemma length_filter_map[simp]: 

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

1054 
by (simp add:filter_map) 

1055 

13142  1056 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1057 
by auto 
13114  1058 

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

1061 
proof (induct xs) 

1062 
case Nil thus ?case by simp 

1063 
next 

1064 
case (Cons x xs) thus ?case 

1065 
apply (auto split:split_if_asm) 

1066 
using length_filter_le[of P xs] apply arith 

1067 
done 

1068 
qed 

13114  1069 

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

1072 
proof (induct xs) 

1073 
case Nil thus ?case by simp 

1074 
next 

1075 
case (Cons x xs) 

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

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

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

1079 
proof (cases) 

1080 
assume "p x" 

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

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

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

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

1089 
finally show ?thesis . 

1090 
next 

1091 
assume "\<not> p x" 

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

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

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

1099 
by (simp add:card_insert_if) 

1100 
finally show ?thesis . 

1101 
qed 

1102 
qed 

1103 

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

1106 
\<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  1107 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1108 
proof(induct ys) 
1109 
case Nil thus ?case by simp 

1110 
next 

1111 
case (Cons y ys) 

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

1113 
proof cases 

1114 
assume Py: "P y" 

1115 
show ?thesis 

1116 
proof cases 

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

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

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

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

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

1122 
with Py Cons.prems show ?thesis by simp 
17629  1123 
qed 
1124 
next 

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

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

1126 
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

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

1128 
then show ?thesis .. 
17629  1129 
qed 
1130 
qed 

1131 

1132 
lemma filter_eq_ConsD: 

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

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

1135 
by(rule Cons_eq_filterD) simp 

1136 

1137 
lemma filter_eq_Cons_iff: 

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

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

1140 
by(auto dest:filter_eq_ConsD) 

1141 

1142 
lemma Cons_eq_filter_iff: 

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

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

1145 
by(auto dest:Cons_eq_filterD) 

1146 

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

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

1150 
apply(erule thin_rl) 

1151 
by (induct ys) simp_all 

1152 

15281  1153 

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

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

1155 

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

1156 
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

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

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

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

1160 
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

1161 

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

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

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

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

1165 

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

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

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

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

1169 

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

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

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

1172 
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

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

1174 
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

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

1176 
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

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

1178 

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

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

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

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

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

1183 
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

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

1185 
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

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

1187 

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

1188 
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

1189 
"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

1190 
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

1191 
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

1192 

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

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

1194 

15392  1195 
subsubsection {* @{text concat} *} 
13114  1196 

13142  1197 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1198 
by (induct xs) auto 
13114  1199 

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

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

24308  1206 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1207 
by (induct xs) auto 
13114  1208 

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

1209 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1210 
by (induct xs) auto 
1211 

13142  1212 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1213 
by (induct xs) auto 
13114  1214 

13142  1215 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1216 
by (induct xs) auto 
13114  1217 

13142  1218 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1219 
by (induct xs) auto 
13114  1220 

1221 

15392  1222 
subsubsection {* @{text nth} *} 
13114  1223 

29827  1224 
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" 
13145  1225 
by auto 
13114  1226 

29827  1227 
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n" 
13145  1228 
by auto 
13114  1229 

13142  1230 
declare nth.simps [simp del] 
13114  1231 

1232 
lemma nth_append: 

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

14208  1235 
apply (case_tac n, auto) 
13145  1236 
done 
13114  1237 

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

1238 
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

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

1240 

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

1241 
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

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

1243 

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

14208  1246 
apply (case_tac n, auto) 
13145  1247 
done 
13114  1248 

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

1251 

18049  1252 

1253 
lemma list_eq_iff_nth_eq: 

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

24632  1256 
apply force 
18049  1257 
apply(case_tac ys) 
1258 
apply simp 

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

1260 
done 

1261 

13142  1262 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  1263 
apply (induct xs, simp, simp) 
13145  1264 
apply safe 
24632  1265 
apply (metis nat_case_0 nth.simps zero_less_Suc) 
1266 
apply (metis less_Suc_eq_0_disj nth_Cons_Suc) 

14208  1267 
apply (case_tac i, simp) 
24632  1268 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1269 
done 
13114  1270 

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

1273 

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

13114  1276 

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

1280 
lemma all_nth_imp_all_set: 

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

13114  1283 

1284 
lemma all_set_conv_all_nth: 

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

13114  1287 

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

1290 
proof (induct xs arbitrary: n) 

1291 
case Nil thus ?case by simp 

1292 
next 

1293 
case (Cons x xs) 

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

1295 
moreover 

1296 
{ assume "n < length xs" 

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

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

1299 
moreover 

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

1301 
ultimately 

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

1303 
} 

1304 
ultimately 

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

1306 
qed 

13114  1307 

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

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

1311 
proof(induct k) 

1312 
case 0 show ?case by simp 

1313 
next 

1314 
case (Suc k) 

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

1316 
proof 

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

1318 
next 

1319 
assume "?L" 

1320 
with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq) 

1321 
hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq) 

1322 
thus "?R" .. 

1323 
qed 

1324 
qed 

1325 

1326 

15392  1327 
subsubsection {* @{text list_update} *} 
13114  1328 

24526  1329 
lemma length_list_update [simp]: "length(xs[i:=x]) = length xs" 
1330 
by (induct xs arbitrary: i) (auto split: nat.split) 

13114  1331 

1332 
lemma nth_list_update: 

24526  1333 
"i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)" 
1334 
by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split) 

13114  1335 

13142  1336 
lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x" 
13145  1337 
by (simp add: nth_list_update) 
13114  1338 

24526  1339 
lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j" 
1340 
by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split) 

13114  1341 

24526  1342 
lemma list_update_id[simp]: "xs[i := xs!i] = xs" 