author  haftmann 
Sat, 06 Mar 2010 09:58:33 +0100  
changeset 35608  db4045d1406e 
parent 35603  c0db094d0d80 
child 35827  f552152d7747 
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 

35608  293 
definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
294 
"insort_insert x xs = (if x \<in> set xs then xs else insort x xs)" 

295 

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

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

297 

24616  298 

23388  299 
subsubsection {* List comprehension *} 
23192  300 

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

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

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

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

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

307 

308 
The qualifiers after the dot are 

309 
\begin{description} 

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

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

311 
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

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

313 
%\item[local bindings] @ {text"let x = e"}. 
24349  314 
\end{description} 
23240  315 

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

316 
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

317 
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

318 
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

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

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

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

324 
definitions for the list comprehensions in question. *} 

325 

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

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

332 

23240  333 
nonterminals lc_qual lc_quals 
23192  334 

335 
syntax 

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

339 
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*) 
23240  340 
"_lc_end" :: "lc_quals" ("]") 
341 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 

24349  342 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  343 

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

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

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

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

24349  353 
"_listcompr e (_lc_let b) (_lc_quals Q Qs)" 
354 
=> "_Let b (_listcompr e Q Qs)" 

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

355 
*) 
23240  356 

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

357 
syntax (xsymbols) 
24349  358 
"_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

359 
syntax (HTML output) 
24349  360 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
361 

362 
parse_translation (advanced) {* 

363 
let 

35256  364 
val NilC = Syntax.const @{const_syntax Nil}; 
365 
val ConsC = Syntax.const @{const_syntax Cons}; 

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

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

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

35115  369 

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

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

371 

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

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

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

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

24349  382 
in lambda x ft end; 
383 

35256  384 
fun abs_tr ctxt (p as Free (s, T)) e opti = 
35115  385 
let 
386 
val thy = ProofContext.theory_of ctxt; 

387 
val s' = Sign.intern_const thy s; 

388 
in 

389 
if Sign.declared_const thy s' 

390 
then (pat_tr ctxt p e opti, false) 

391 
else (lambda p e, true) 

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

393 
 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

394 

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

397 
val res = 

398 
(case qs of 

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

400 
 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

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

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

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

405 
(case abs_tr ctxt p e true of 
35115  406 
(f, true) => mapC $ f $ es 
407 
 (f, false) => concatC $ (mapC $ f $ es)) 

408 
 lc_tr ctxt 

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

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

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

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

413 

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

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

416 

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

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

419 
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

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

421 
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

422 
term "[(x,y,z). x<a, x\<leftarrow>xs]" 
24349  423 
term "[(x,y). Cons True x \<leftarrow> xs]" 
424 
term "[(x,y,z). Cons x [] \<leftarrow> xs]" 

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

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

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

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

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

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

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

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

35115  437 

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

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

439 

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

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

441 
"xs \<noteq> x # xs" 
13145  442 
by (induct xs) auto 
13114  443 

13142  444 
lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] 
13114  445 

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

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

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

453 

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

454 
subsubsection {* @{const length} *} 
13114  455 

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

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

458 
append_eq_append_conv}. 
13142  459 
*} 
13114  460 

13142  461 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  462 
by (induct xs) auto 
13114  463 

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

13142  467 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  468 
by (induct xs) auto 
13114  469 

13142  470 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  471 
by (cases xs) auto 
13114  472 

13142  473 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  474 
by (induct xs) auto 
13114  475 

13142  476 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  477 
by (induct xs) auto 
13114  478 

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

481 

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

13142  485 

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

14208  488 
apply (induct xs, simp, simp) 
14025  489 
apply blast 
490 
done 

491 

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

492 
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

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

494 

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

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

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

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

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

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

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

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

502 
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

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

504 

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

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

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

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

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

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

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

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

512 
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

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

514 
qed 
13114  515 

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

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

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

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

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

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

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

522 
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

523 

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

524 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  525 
by (rule Eq_FalseI) auto 
24037  526 

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

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

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

529 
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

530 
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

531 
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

532 
*) 
24037  533 

534 
let 

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

535 

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

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

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

540 
 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

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

542 

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

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

546 
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

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

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

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

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

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

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

556 
in 
23214  557 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
558 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

563 

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

564 

15392  565 
subsubsection {* @{text "@"}  append *} 
13114  566 

13142  567 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  568 
by (induct xs) auto 
13114  569 

13142  570 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  571 
by (induct xs) auto 
3507  572 

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

13142  576 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  577 
by (induct xs) auto 
13114  578 

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

13142  582 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  583 
by (induct xs) auto 
13114  584 

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

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

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

13145  591 
done 
13142  592 

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

595 
apply (induct xs arbitrary: ys zs ts) 

14495  596 
apply fastsimp 
597 
apply(case_tac zs) 

598 
apply simp 

599 
apply fastsimp 

600 
done 

601 

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

602 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  603 
by simp 
13142  604 

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

13145  606 
by simp 
13114  607 

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

608 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  609 
by simp 
13114  610 

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

13142  614 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  615 
using append_same_eq [of "[]"] by auto 
13114  616 

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

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

13142  620 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  621 
by (induct xs) auto 
13114  622 

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

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

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

632 

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

635 
by(cases ys) auto 

636 

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

639 
by(cases ys) auto 

640 

14300  641 

13142  642 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  643 

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

13145  645 
by simp 
13114  646 

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

13114  650 

13142  651 
lemma append_eq_appendI: 
13145  652 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
653 
by (drule sym) simp 

13114  654 

655 

13142  656 
text {* 
13145  657 
Simplification procedure for all list equalities. 
658 
Currently only tries to rearrange @{text "@"} to see if 

659 
 both lists end in a singleton list, 

660 
 or both lists end in the same list. 

13142  661 
*} 
662 

26480  663 
ML {* 
3507  664 
local 
665 

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

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

13462  669 
 last t = t; 
13114  670 

29856  671 
fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true 
13462  672 
 list1 _ = false; 
13114  673 

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

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

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

13114  678 

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

16973  681 

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

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

685 
fun rearr conv = 

686 
let 

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

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

689 
val appT = [listT,listT] > listT 

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

692 
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

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

694 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  695 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  696 

13462  697 
in 
22633  698 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
699 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  700 
else NONE 
13462  701 
end; 
702 

13114  703 
in 
13462  704 

705 
val list_eq_simproc = 

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

13114  708 
end; 
709 

710 
Addsimprocs [list_eq_simproc]; 

711 
*} 

712 

713 

15392  714 
subsubsection {* @{text map} *} 
13114  715 

13142  716 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  717 
by (induct xs) simp_all 
13114  718 

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

13142  722 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  723 
by (induct xs) auto 
13114  724 

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

725 
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

726 
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

727 

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

730 
apply(simp) 

731 
done 

732 

13142  733 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  734 
by (induct xs) auto 
13114  735 

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

738 

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

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

13737  742 
by simp 
13114  743 

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

13142  747 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  748 
by (cases xs) auto 
13114  749 

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

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

757 

18447  758 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
759 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

760 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

761 

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

18447  764 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  765 

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

766 
lemma map_eq_imp_length_eq: 
35510  767 
assumes "map f xs = map g ys" 
26734  768 
shows "length xs = length ys" 
769 
using assms proof (induct ys arbitrary: xs) 

770 
case Nil then show ?case by simp 

771 
next 

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

35510  773 
from Cons xs have "map f zs = map g ys" by simp 
26734  774 
moreover with Cons have "length zs = length ys" by blast 
775 
with xs show ?case by simp 

776 
qed 

777 

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

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

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

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

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

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

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

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

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

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

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

788 

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

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

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

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

792 

13114  793 
lemma map_injective: 
24526  794 
"map f xs = map f ys ==> inj f ==> xs = ys" 
795 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  796 

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

799 

13114  800 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  801 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  802 

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

14208  804 
apply (unfold inj_on_def, clarify) 
13145  805 
apply (erule_tac x = "[x]" in ballE) 
14208  806 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  807 
apply blast 
808 
done 

13114  809 

14339  810 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  811 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  812 

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

815 
apply(erule map_inj_on) 

816 
apply(blast intro:inj_onI dest:inj_onD) 

817 
done 

818 

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

13114  821 

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

822 
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

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

824 

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

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

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

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

828 

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

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

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

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

832 

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

833 

15392  834 
subsubsection {* @{text rev} *} 
13114  835 

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

13142  839 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  840 
by (induct xs) auto 
13114  841 

15870  842 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
843 
by auto 

844 

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

13142  848 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  849 
by (induct xs) auto 
13114  850 

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

853 

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

855 
by (cases xs) auto 

856 

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

857 
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

858 
apply (induct xs arbitrary: ys, force) 
14208  859 
apply (case_tac ys, simp, force) 
13145  860 
done 
13114  861 

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

864 

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

867 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  868 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
869 
done 

13114  870 

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

13145  873 
by (induct xs rule: rev_induct) auto 
13114  874 

13366  875 
lemmas rev_cases = rev_exhaust 
876 

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

879 

13114  880 

15392  881 
subsubsection {* @{text set} *} 
13114  882 

13142  883 
lemma finite_set [iff]: "finite (set xs)" 
13145  884 
by (induct xs) auto 
13114  885 

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

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

14099  891 

13142  892 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  893 
by auto 
13114  894 

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

897 

13142  898 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  899 
by (induct xs) auto 
13114  900 

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

903 

13142  904 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  905 
by (induct xs) auto 
13114  906 

13142  907 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  908 
by (induct xs) auto 
13114  909 

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

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

13114  915 

13142  916 

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

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

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

922 
qed 

923 

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

26073  926 

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

928 
proof (induct xs) 

929 
case Nil thus ?case by simp 

18049  930 
next 
931 
case (Cons a xs) 

932 
show ?case 

933 
proof cases 

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

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

938 
qed 

939 

940 
lemma in_set_conv_decomp_first: 

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

26734  942 
by (auto dest!: split_list_first) 
26073  943 

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

945 
proof (induct xs rule:rev_induct) 

946 
case Nil thus ?case by simp 

947 
next 

948 
case (snoc a xs) 

949 
show ?case 

950 
proof cases 

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

952 
next 

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

18049  954 
qed 
955 
qed 

956 

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

26734  959 
by (auto dest!: split_list_last) 
26073  960 

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

962 
proof (induct xs) 

963 
case Nil thus ?case by simp 

964 
next 

965 
case Cons thus ?case 

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

967 
qed 

968 

969 
lemma split_list_propE: 

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

972 
using split_list_prop [OF assms] by blast 

26073  973 

974 
lemma split_list_first_prop: 

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

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

26734  977 
proof (induct xs) 
26073  978 
case Nil thus ?case by simp 
979 
next 

980 
case (Cons x xs) 

981 
show ?case 

982 
proof cases 

983 
assume "P x" 

26734  984 
thus ?thesis by simp 
985 
(metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 

26073  986 
next 
987 
assume "\<not> P x" 

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

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

990 
qed 

991 
qed 

992 

993 
lemma split_list_first_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>y \<in> set ys. \<not> P y" 

996 
using split_list_first_prop [OF assms] by blast 

26073  997 

998 
lemma split_list_first_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>y \<in> set ys. \<not> P y))" 

26734  1001 
by (rule, erule split_list_first_prop) auto 
26073  1002 

1003 
lemma split_list_last_prop: 

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

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

1006 
proof(induct xs rule:rev_induct) 

1007 
case Nil thus ?case by simp 

1008 
next 

1009 
case (snoc x xs) 

1010 
show ?case 

1011 
proof cases 

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

1013 
next 

1014 
assume "\<not> P x" 

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

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

1017 
qed 

1018 
qed 

1019 

1020 
lemma split_list_last_propE: 

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

1023 
using split_list_last_prop [OF assms] by blast 

26073  1024 

1025 
lemma split_list_last_prop_iff: 

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

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

26734  1028 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1029 

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

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

13508  1033 

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

13114  1036 

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

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

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

1039 
by (induct xs) auto 
15168  1040 

35115  1041 

15392  1042 
subsubsection {* @{text filter} *} 
13114  1043 

13142  1044 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1045 
by (induct xs) auto 
13114  1046 

15305  1047 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1048 
by (induct xs) simp_all 

1049 

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

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

1055 

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

1058 
by(induct xs) simp_all 

1059 

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

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

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

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

1070 
apply (induct xs) 

1071 
apply auto 

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

1073 
apply simp 

1074 
done 

13114  1075 

16965  1076 
lemma filter_map: 
1077 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1078 
by (induct xs) simp_all 

1079 

1080 
lemma length_filter_map[simp]: 

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

1082 
by (simp add:filter_map) 

1083 

13142  1084 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1085 
by auto 
13114  1086 

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

1089 
proof (induct xs) 

1090 
case Nil thus ?case by simp 

1091 
next 

1092 
case (Cons x xs) thus ?case 

1093 
apply (auto split:split_if_asm) 

1094 
using length_filter_le[of P xs] apply arith 

1095 
done 

1096 
qed 

13114  1097 

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

1100 
proof (induct xs) 

1101 
case Nil thus ?case by simp 

1102 
next 

1103 
case (Cons x xs) 

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

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

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

1107 
proof (cases) 

1108 
assume "p x" 

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

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

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

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

1117 
finally show ?thesis . 

1118 
next 

1119 
assume "\<not> p x" 

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

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

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

1127 
by (simp add:card_insert_if) 

1128 
finally show ?thesis . 

1129 
qed 

1130 
qed 

1131 

17629  1132 
lemma Cons_eq_filterD: 
1133 
"x#xs = filter P ys \<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" 

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

1138 
next 

1139 
case (Cons y ys) 

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

1141 
proof cases 

1142 
assume Py: "P y" 

1143 
show ?thesis 

1144 
proof cases 

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

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

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

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

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

1150 
with Py Cons.prems show ?thesis by simp 
17629  1151 
qed 
1152 
next 

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

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

1154 
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

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

1156 
then show ?thesis .. 
17629  1157 
qed 
1158 
qed 

1159 

1160 
lemma filter_eq_ConsD: 

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

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

1163 
by(rule Cons_eq_filterD) simp 

1164 

1165 
lemma filter_eq_Cons_iff: 

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

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

1168 
by(auto dest:filter_eq_ConsD) 

1169 

1170 
lemma Cons_eq_filter_iff: 

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

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

1173 
by(auto dest:Cons_eq_filterD) 

1174 

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

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

1178 
apply(erule thin_rl) 

1179 
by (induct ys) simp_all 

1180 

15281  1181 

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

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

1183 

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

1184 
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

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

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

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

1188 
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

1189 

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

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

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

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

1193 

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

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

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

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

1197 

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

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

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

1200 
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

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

1202 
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

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

1204 
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

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

1206 

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

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

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

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

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

1211 
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

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

1213 
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

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

1215 

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

1216 
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

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

1218 
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

1219 
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

1220 

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

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

1222 

35115  1223 

15392  1224 
subsubsection {* @{text concat} *} 
13114  1225 

13142  1226 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1227 
by (induct xs) auto 
13114  1228 

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

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

24308  1235 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1236 
by (induct xs) auto 
13114  1237 

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

1238 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1239 
by (induct xs) auto 
1240 

13142  1241 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1242 
by (induct xs) auto 
13114  1243 

13142  1244 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1245 
by (induct xs) auto 
13114  1246 

13142  1247 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1248 
by (induct xs) auto 
13114  1249 

1250 

15392  1251 
subsubsection {* @{text nth} *} 
13114  1252 

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

29827  1256 
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n" 
13145  1257 
by auto 
13114  1258 

13142  1259 
declare nth.simps [simp del] 
13114  1260 

1261 
lemma nth_append: 

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

14208  1264 
apply (case_tac n, auto) 
13145  1265 
done 
13114  1266 

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

1267 
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

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

1269 

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

1270 
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

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

1272 

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

14208  1275 
apply (case_tac n, auto) 
13145  1276 
done 
13114  1277 

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

1280 

18049  1281 

1282 
lemma list_eq_iff_nth_eq: 

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

24632  1285 
apply force 
18049  1286 
apply(case_tac ys) 
1287 
apply simp 

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

1289 
done 

1290 

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

14208  1296 
apply (case_tac i, simp) 
24632  1297 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1298 
done 
13114  1299 

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

1302 

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

13114  1305 

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

1309 
lemma all_nth_imp_all_set: 

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

13114  1312 

1313 
lemma all_set_conv_all_nth: 

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

13114  1316 

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

1319 
proof (induct xs arbitrary: n) 

1320 
case Nil thus ?case by simp 

1321 
next 

1322 
case (Cons x xs) 

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

1324 
moreover 

1325 
{ assume "n < length xs" 

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

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

1328 
moreover 

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

1330 
ultimately 

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

1332 
} 

1333 
ultimately 

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

1335 
qed 

13114  1336 

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

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

1340 
proof(induct k) 

1341 
case 0 show ?case by simp 

1342 
next 

1343 