author  wenzelm 
Fri, 16 Apr 2010 21:28:09 +0200  
changeset 36176  3fe7e97ccca8 
parent 36154  11c6106d7787 
child 36199  4d220994f30b 
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 
35827  8 
imports Plain Presburger Sledgehammer 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 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36154
diff
changeset

175 
hide_const (open) insert 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36154
diff
changeset

176 
hide_fact (open) insert_def 
34978
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

177 

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

180 
"remove1 x [] = []" 

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

182 

183 
primrec 

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

185 
"removeAll x [] = []" 

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

187 

188 
primrec 

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

190 
replicate_0: "replicate 0 x = []" 

191 
 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

192 

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

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

15307  200 

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

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

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

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

204 

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

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

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

208 

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

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

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

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

213 

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

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

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

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

218 
primrec 

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

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

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

223 

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

226 
\fbox{ 

227 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

252 
@{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

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

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

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

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

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

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

267 
\label{fig:Characteristic} 

268 
\end{figure} 

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

272 

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

275 

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

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

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

278 

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

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

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

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

284 
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

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

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

287 

35195  288 
definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
289 
"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

290 

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

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

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

296 

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

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

298 

24616  299 

23388  300 
subsubsection {* List comprehension *} 
23192  301 

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

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

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

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

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

308 

309 
The qualifiers after the dot are 

310 
\begin{description} 

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

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

312 
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

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

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

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

317 
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

318 
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

319 
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

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

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

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

325 
definitions for the list comprehensions in question. *} 

326 

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

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

333 

23240  334 
nonterminals lc_qual lc_quals 
23192  335 

336 
syntax 

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

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

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

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

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

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

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

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

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

356 
*) 
23240  357 

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

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

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

363 
parse_translation (advanced) {* 

364 
let 

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

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

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

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

35115  370 

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

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

372 

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

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

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

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

24349  383 
in lambda x ft end; 
384 

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

388 
val s' = Sign.intern_const thy s; 

389 
in 

390 
if Sign.declared_const thy s' 

391 
then (pat_tr ctxt p e opti, false) 

392 
else (lambda p e, true) 

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

394 
 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

395 

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

398 
val res = 

399 
(case qs of 

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

401 
 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

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

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

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

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

409 
 lc_tr ctxt 

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

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

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

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

414 

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

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

417 

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

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

420 
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

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

422 
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

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

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

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

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

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

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

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

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

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

35115  438 

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

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

440 

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

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

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

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

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

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

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

454 

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

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

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

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

459 
append_eq_append_conv}. 
13142  460 
*} 
13114  461 

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

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

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

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

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

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

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

482 

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

13142  486 

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

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

492 

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

493 
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

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

495 

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

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

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

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

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

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

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

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

503 
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

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

505 

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

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

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

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

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

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

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

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

513 
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

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

515 
qed 
13114  516 

36154
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

517 
lemma list_induct4 [consumes 3, case_names Nil Cons]: 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

518 
"length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

519 
P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow> 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

520 
length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow> 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

521 
P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws" 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

522 
proof (induct xs arbitrary: ys zs ws) 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

523 
case Nil then show ?case by simp 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

524 
next 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

525 
case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all) 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

526 
qed 
11c6106d7787
Respectfullness and preservation of list_rel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35828
diff
changeset

527 

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

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

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

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

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

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

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

534 
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

535 

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

536 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  537 
by (rule Eq_FalseI) auto 
24037  538 

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

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

542 
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

543 
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

544 
*) 
24037  545 

546 
let 

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

547 

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

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

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

552 
 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

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

554 

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

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

558 
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

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

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

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

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

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

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

568 
in 
23214  569 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
570 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

575 

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

576 

15392  577 
subsubsection {* @{text "@"}  append *} 
13114  578 

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

13142  582 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  583 
by (induct xs) auto 
3507  584 

13142  585 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  586 
by (induct xs) auto 
13114  587 

13142  588 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  589 
by (induct xs) auto 
13114  590 

13142  591 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  592 
by (induct xs) auto 
13114  593 

13142  594 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  595 
by (induct xs) auto 
13114  596 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35827
diff
changeset

597 
lemma append_eq_append_conv [simp, no_atp]: 
24526  598 
"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

599 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  600 
apply (induct xs arbitrary: ys) 
14208  601 
apply (case_tac ys, simp, force) 
602 
apply (case_tac ys, force, simp) 

13145  603 
done 
13142  604 

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

607 
apply (induct xs arbitrary: ys zs ts) 

14495  608 
apply fastsimp 
609 
apply(case_tac zs) 

610 
apply simp 

611 
apply fastsimp 

612 
done 

613 

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

614 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  615 
by simp 
13142  616 

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

13145  618 
by simp 
13114  619 

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

620 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  621 
by simp 
13114  622 

13142  623 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  624 
using append_same_eq [of _ _ "[]"] by auto 
3507  625 

13142  626 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  627 
using append_same_eq [of "[]"] by auto 
13114  628 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35827
diff
changeset

629 
lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
13145  630 
by (induct xs) auto 
13114  631 

13142  632 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  633 
by (induct xs) auto 
13114  634 

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

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

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

644 

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

647 
by(cases ys) auto 

648 

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

651 
by(cases ys) auto 

652 

14300  653 

13142  654 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  655 

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

13145  657 
by simp 
13114  658 

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

13114  662 

13142  663 
lemma append_eq_appendI: 
13145  664 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
665 
by (drule sym) simp 

13114  666 

667 

13142  668 
text {* 
13145  669 
Simplification procedure for all list equalities. 
670 
Currently only tries to rearrange @{text "@"} to see if 

671 
 both lists end in a singleton list, 

672 
 or both lists end in the same list. 

13142  673 
*} 
674 

26480  675 
ML {* 
3507  676 
local 
677 

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

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

13462  681 
 last t = t; 
13114  682 

29856  683 
fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true 
13462  684 
 list1 _ = false; 
13114  685 

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

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

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

13114  690 

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

16973  693 

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

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

697 
fun rearr conv = 

698 
let 

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

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

701 
val appT = [listT,listT] > listT 

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

704 
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

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

706 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  707 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  708 

13462  709 
in 
22633  710 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
711 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  712 
else NONE 
13462  713 
end; 
714 

13114  715 
in 
13462  716 

717 
val list_eq_simproc = 

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

13114  720 
end; 
721 

722 
Addsimprocs [list_eq_simproc]; 

723 
*} 

724 

725 

15392  726 
subsubsection {* @{text map} *} 
13114  727 

13142  728 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  729 
by (induct xs) simp_all 
13114  730 

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

13142  734 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  735 
by (induct xs) auto 
13114  736 

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

737 
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

738 
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

739 

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

742 
apply(simp) 

743 
done 

744 

13142  745 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  746 
by (induct xs) auto 
13114  747 

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

750 

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

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

13737  754 
by simp 
13114  755 

13142  756 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  757 
by (cases xs) auto 
13114  758 

13142  759 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  760 
by (cases xs) auto 
13114  761 

18447  762 
lemma map_eq_Cons_conv: 
14025  763 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  764 
by (cases xs) auto 
13114  765 

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

769 

18447  770 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
771 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

772 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

773 

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

18447  776 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  777 

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

778 
lemma map_eq_imp_length_eq: 
35510  779 
assumes "map f xs = map g ys" 
26734  780 
shows "length xs = length ys" 
781 
using assms proof (induct ys arbitrary: xs) 

782 
case Nil then show ?case by simp 

783 
next 

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

35510  785 
from Cons xs have "map f zs = map g ys" by simp 
26734  786 
moreover with Cons have "length zs = length ys" by blast 
787 
with xs show ?case by simp 

788 
qed 

789 

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

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

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

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

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

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

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

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

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

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

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

800 

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

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

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

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

804 

13114  805 
lemma map_injective: 
24526  806 
"map f xs = map f ys ==> inj f ==> xs = ys" 
807 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  808 

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

811 

13114  812 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  813 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  814 

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

14208  816 
apply (unfold inj_on_def, clarify) 
13145  817 
apply (erule_tac x = "[x]" in ballE) 
14208  818 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  819 
apply blast 
820 
done 

13114  821 

14339  822 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  823 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  824 

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

827 
apply(erule map_inj_on) 

828 
apply(blast intro:inj_onI dest:inj_onD) 

829 
done 

830 

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

13114  833 

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

834 
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

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

836 

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

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

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

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

840 

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

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

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

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

844 

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

845 

15392  846 
subsubsection {* @{text rev} *} 
13114  847 

13142  848 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  849 
by (induct xs) auto 
13114  850 

13142  851 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  852 
by (induct xs) auto 
13114  853 

15870  854 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
855 
by auto 

856 

13142  857 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  858 
by (induct xs) auto 
13114  859 

13142  860 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  861 
by (induct xs) auto 
13114  862 

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

865 

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

867 
by (cases xs) auto 

868 

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

869 
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

870 
apply (induct xs arbitrary: ys, force) 
14208  871 
apply (case_tac ys, simp, force) 
13145  872 
done 
13114  873 

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

876 

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

879 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  880 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
881 
done 

13114  882 

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

13145  885 
by (induct xs rule: rev_induct) auto 
13114  886 

13366  887 
lemmas rev_cases = rev_exhaust 
888 

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

891 

13114  892 

15392  893 
subsubsection {* @{text set} *} 
13114  894 

13142  895 
lemma finite_set [iff]: "finite (set xs)" 
13145  896 
by (induct xs) auto 
13114  897 

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

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

14099  903 

13142  904 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  905 
by auto 
13114  906 

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

909 

13142  910 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  911 
by (induct xs) auto 
13114  912 

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

915 

13142  916 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  917 
by (induct xs) auto 
13114  918 

13142  919 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  920 
by (induct xs) auto 
13114  921 

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

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

13114  927 

13142  928 

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

929 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  930 
proof (induct xs) 
26073  931 
case Nil thus ?case by simp 
932 
next 

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

934 
qed 

935 

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

26073  938 

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

940 
proof (induct xs) 

941 
case Nil thus ?case by simp 

18049  942 
next 
943 
case (Cons a xs) 

944 
show ?case 

945 
proof cases 

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

946 
assume "x = a" thus ?case using Cons by fastsimp 
18049  947 
next 
26073  948 
assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI) 
949 
qed 

950 
qed 

951 

952 
lemma in_set_conv_decomp_first: 

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

26734  954 
by (auto dest!: split_list_first) 
26073  955 

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

957 
proof (induct xs rule:rev_induct) 

958 
case Nil thus ?case by simp 

959 
next 

960 
case (snoc a xs) 

961 
show ?case 

962 
proof cases 

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

964 
next 

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

18049  966 
qed 
967 
qed 

968 

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

26734  971 
by (auto dest!: split_list_last) 
26073  972 

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

974 
proof (induct xs) 

975 
case Nil thus ?case by simp 

976 
next 

977 
case Cons thus ?case 

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

979 
qed 

980 

981 
lemma split_list_propE: 

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

984 
using split_list_prop [OF assms] by blast 

26073  985 

986 
lemma split_list_first_prop: 

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

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

26734  989 
proof (induct xs) 
26073  990 
case Nil thus ?case by simp 
991 
next 

992 
case (Cons x xs) 

993 
show ?case 

994 
proof cases 

995 
assume "P x" 

26734  996 
thus ?thesis by simp 
997 
(metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 

26073  998 
next 
999 
assume "\<not> P x" 

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

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

1002 
qed 

1003 
qed 

1004 

1005 
lemma split_list_first_propE: 

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

1008 
using split_list_first_prop [OF assms] by blast 

26073  1009 

1010 
lemma split_list_first_prop_iff: 

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

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

26734  1013 
by (rule, erule split_list_first_prop) auto 
26073  1014 

1015 
lemma split_list_last_prop: 

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

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

1018 
proof(induct xs rule:rev_induct) 

1019 
case Nil thus ?case by simp 

1020 
next 

1021 
case (snoc x xs) 

1022 
show ?case 

1023 
proof cases 

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

1025 
next 

1026 
assume "\<not> P x" 

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

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

1029 
qed 

1030 
qed 

1031 

1032 
lemma split_list_last_propE: 

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

1035 
using split_list_last_prop [OF assms] by blast 

26073  1036 

1037 
lemma split_list_last_prop_iff: 

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

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

26734  1040 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1041 

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

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

13508  1045 

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

13114  1048 

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

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

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

1051 
by (induct xs) auto 
15168  1052 

35115  1053 

15392  1054 
subsubsection {* @{text filter} *} 
13114  1055 

13142  1056 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1057 
by (induct xs) auto 
13114  1058 

15305  1059 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1060 
by (induct xs) simp_all 

1061 

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

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

1067 

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

1070 
by(induct xs) simp_all 

1071 

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

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

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

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

1082 
apply (induct xs) 

1083 
apply auto 

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

1085 
apply simp 

1086 
done 

13114  1087 

16965  1088 
lemma filter_map: 
1089 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1090 
by (induct xs) simp_all 

1091 

1092 
lemma length_filter_map[simp]: 

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

1094 
by (simp add:filter_map) 

1095 

13142  1096 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1097 
by auto 
13114  1098 

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

1101 
proof (induct xs) 

1102 
case Nil thus ?case by simp 

1103 
next 

1104 
case (Cons x xs) thus ?case 

1105 
apply (auto split:split_if_asm) 

1106 
using length_filter_le[of P xs] apply arith 

1107 
done 

1108 
qed 

13114  1109 

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

1112 
proof (induct xs) 

1113 
case Nil thus ?case by simp 

1114 
next 

1115 
case (Cons x xs) 

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

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

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

1119 
proof (cases) 

1120 
assume "p x" 

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

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

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

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

1129 
finally show ?thesis . 

1130 
next 

1131 
assume "\<not> p x" 

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

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

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

1139 
by (simp add:card_insert_if) 

1140 
finally show ?thesis . 

1141 
qed 

1142 
qed 

1143 

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

1146 
\<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  1147 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1148 
proof(induct ys) 
1149 
case Nil thus ?case by simp 

1150 
next 

1151 
case (Cons y ys) 

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

1153 
proof cases 

1154 
assume Py: "P y" 

1155 
show ?thesis 

1156 
proof cases 

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

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

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

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

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

1162 
with Py Cons.prems show ?thesis by simp 
17629  1163 
qed 
1164 
next 

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

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

1166 
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

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

1168 
then show ?thesis .. 
17629  1169 
qed 
1170 
qed 

1171 

1172 
lemma filter_eq_ConsD: 

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

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

1175 
by(rule Cons_eq_filterD) simp 

1176 

1177 
lemma filter_eq_Cons_iff: 

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

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

1180 
by(auto dest:filter_eq_ConsD) 

1181 

1182 
lemma Cons_eq_filter_iff: 

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

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

1185 
by(auto dest:Cons_eq_filterD) 

1186 

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

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

1190 
apply(erule thin_rl) 

1191 
by (induct ys) simp_all 

1192 

15281  1193 

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

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

1195 

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

1196 
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

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

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

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

1200 
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

1201 

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

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

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

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

1205 

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

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

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

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

1209 

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

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

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

1212 
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

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

1214 
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

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

1216 
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

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

1218 

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

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

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

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

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

1223 
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

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

1225 
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

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

1227 

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

1228 
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

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

1230 
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

1231 
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

1232 

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

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

1234 

35115  1235 

15392  1236 
subsubsection {* @{text concat} *} 
13114  1237 

13142  1238 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1239 
by (induct xs) auto 
13114  1240 

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

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

24308  1247 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1248 
by (induct xs) auto 
13114  1249 

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

1250 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1251 
by (induct xs) auto 
1252 

13142  1253 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1254 
by (induct xs) auto 
13114  1255 

13142  1256 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1257 
by (induct xs) auto 
13114  1258 

13142  1259 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1260 
by (induct xs) auto 
13114  1261 

1262 

15392  1263 
subsubsection {* @{text nth} *} 
13114  1264 

29827  1265 
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" 
13145  1266 
by auto 
13114  1267 

29827  1268 
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n" 
13145  1269 
by auto 
13114  1270 

13142  1271 
declare nth.simps [simp del] 
13114  1272 

1273 
lemma nth_append: 

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

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

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

1279 
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

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

1281 

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

1282 
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

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

1284 

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

14208  1287 
apply (case_tac n, auto) 
13145  1288 
done 
13114  1289 

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

1292 

18049  1293 

1294 
lemma list_eq_iff_nth_eq: 

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

24632  1297 
apply force 
18049  1298 
apply(case_tac ys) 
1299 
apply simp 

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

1301 
done 

1302 

13142  1303 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  1304 
apply (induct xs, simp, simp) 
13145  1305 
apply safe 
24632  1306 
apply (metis nat_case_0 nth.simps zero_less_Suc) 
1307 
apply (metis less_Suc_eq_0_disj nth_Cons_Suc) 

14208  1308 
apply (case_tac i, simp) 
24632  1309 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1310 
done 
13114  1311 

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

1314 

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

13114  1317 

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

1321 
lemma all_nth_imp_all_set: 

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

13114  1324 

1325 
lemma all_set_conv_all_nth: 

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

13114  1328 

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

1331 
proof (induct xs arbitrary: n) 

1332 
case Nil thus ?case by simp 

1333 
next 

1334 
case (Cons x xs) 

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

1336 
moreover 

1337 
{ assume "n < length xs" 

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