author  hoelzl 
Thu, 02 Sep 2010 10:18:15 +0200  
changeset 39073  8520a1f89db1 
parent 38857  97775f3e8722 
child 39198  f967a16dfcdd 
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 
37457  8 
imports Plain Quotient Presburger Code_Numeral 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 
37767  211 
"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 

37289  454 
lemma list_nonempty_induct [consumes 1, case_names single cons]: 
455 
assumes "xs \<noteq> []" 

456 
assumes single: "\<And>x. P [x]" 

457 
assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)" 

458 
shows "P xs" 

459 
using `xs \<noteq> []` proof (induct xs) 

460 
case Nil then show ?case by simp 

461 
next 

462 
case (Cons x xs) show ?case proof (cases xs) 

463 
case Nil with single show ?thesis by simp 

464 
next 

465 
case Cons then have "xs \<noteq> []" by simp 

466 
moreover with Cons.hyps have "P xs" . 

467 
ultimately show ?thesis by (rule cons) 

468 
qed 

469 
qed 

470 

13114  471 

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

472 
subsubsection {* @{const length} *} 
13114  473 

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

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

476 
append_eq_append_conv}. 
13142  477 
*} 
13114  478 

13142  479 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  480 
by (induct xs) auto 
13114  481 

13142  482 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  483 
by (induct xs) auto 
13114  484 

13142  485 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  486 
by (induct xs) auto 
13114  487 

13142  488 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  489 
by (cases xs) auto 
13114  490 

13142  491 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  492 
by (induct xs) auto 
13114  493 

13142  494 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  495 
by (induct xs) auto 
13114  496 

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

499 

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

13142  503 

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

14208  506 
apply (induct xs, simp, simp) 
14025  507 
apply blast 
508 
done 

509 

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

510 
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

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

512 

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

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

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

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

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

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

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

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

520 
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

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

522 

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

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

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

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

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

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

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

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

530 
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

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

532 
qed 
13114  533 

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

534 
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

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

536 
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

537 
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

538 
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

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

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

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

542 
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

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

544 

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

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

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

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

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

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

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

551 
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

552 

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

553 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  554 
by (rule Eq_FalseI) auto 
24037  555 

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

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

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

558 
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

559 
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

560 
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

561 
*) 
24037  562 

563 
let 

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

564 

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

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

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

569 
 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

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

571 

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

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

575 
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

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

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

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

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

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

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

585 
in 
23214  586 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
587 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

592 

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

593 

15392  594 
subsubsection {* @{text "@"}  append *} 
13114  595 

13142  596 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  597 
by (induct xs) auto 
13114  598 

13142  599 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  600 
by (induct xs) auto 
3507  601 

13142  602 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  603 
by (induct xs) auto 
13114  604 

13142  605 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  606 
by (induct xs) auto 
13114  607 

13142  608 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  609 
by (induct xs) auto 
13114  610 

13142  611 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  612 
by (induct xs) auto 
13114  613 

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

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

616 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  617 
apply (induct xs arbitrary: ys) 
14208  618 
apply (case_tac ys, simp, force) 
619 
apply (case_tac ys, force, simp) 

13145  620 
done 
13142  621 

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

624 
apply (induct xs arbitrary: ys zs ts) 

14495  625 
apply fastsimp 
626 
apply(case_tac zs) 

627 
apply simp 

628 
apply fastsimp 

629 
done 

630 

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

631 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  632 
by simp 
13142  633 

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

13145  635 
by simp 
13114  636 

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

637 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  638 
by simp 
13114  639 

13142  640 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  641 
using append_same_eq [of _ _ "[]"] by auto 
3507  642 

13142  643 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  644 
using append_same_eq [of "[]"] by auto 
13114  645 

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

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

13142  649 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  650 
by (induct xs) auto 
13114  651 

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

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

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

661 

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

664 
by(cases ys) auto 

665 

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

668 
by(cases ys) auto 

669 

14300  670 

13142  671 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  672 

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

13145  674 
by simp 
13114  675 

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

13114  679 

13142  680 
lemma append_eq_appendI: 
13145  681 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
682 
by (drule sym) simp 

13114  683 

684 

13142  685 
text {* 
13145  686 
Simplification procedure for all list equalities. 
687 
Currently only tries to rearrange @{text "@"} to see if 

688 
 both lists end in a singleton list, 

689 
 or both lists end in the same list. 

13142  690 
*} 
691 

26480  692 
ML {* 
3507  693 
local 
694 

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

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

13462  698 
 last t = t; 
13114  699 

29856  700 
fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true 
13462  701 
 list1 _ = false; 
13114  702 

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

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

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

13114  707 

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

16973  710 

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

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

714 
fun rearr conv = 

715 
let 

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

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

718 
val appT = [listT,listT] > listT 

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

721 
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

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

723 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  724 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  725 

13462  726 
in 
22633  727 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
728 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  729 
else NONE 
13462  730 
end; 
731 

13114  732 
in 
13462  733 

734 
val list_eq_simproc = 

38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
37880
diff
changeset

735 
Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq); 
13462  736 

13114  737 
end; 
738 

739 
Addsimprocs [list_eq_simproc]; 

740 
*} 

741 

742 

15392  743 
subsubsection {* @{text map} *} 
13114  744 

13142  745 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  746 
by (induct xs) simp_all 
13114  747 

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

13142  751 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  752 
by (induct xs) auto 
13114  753 

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

754 
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

755 
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

756 

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

759 
apply(simp) 

760 
done 

761 

13142  762 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  763 
by (induct xs) auto 
13114  764 

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

767 

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

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

13737  771 
by simp 
13114  772 

13142  773 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  774 
by (cases xs) auto 
13114  775 

13142  776 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  777 
by (cases xs) auto 
13114  778 

18447  779 
lemma map_eq_Cons_conv: 
14025  780 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  781 
by (cases xs) auto 
13114  782 

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

786 

18447  787 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
788 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

789 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

790 

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

18447  793 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  794 

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

795 
lemma map_eq_imp_length_eq: 
35510  796 
assumes "map f xs = map g ys" 
26734  797 
shows "length xs = length ys" 
798 
using assms proof (induct ys arbitrary: xs) 

799 
case Nil then show ?case by simp 

800 
next 

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

35510  802 
from Cons xs have "map f zs = map g ys" by simp 
26734  803 
moreover with Cons have "length zs = length ys" by blast 
804 
with xs show ?case by simp 

805 
qed 

806 

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

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

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

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

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

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

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

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

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

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

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

817 

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

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

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

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

821 

13114  822 
lemma map_injective: 
24526  823 
"map f xs = map f ys ==> inj f ==> xs = ys" 
824 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  825 

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

828 

13114  829 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  830 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  831 

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

14208  833 
apply (unfold inj_on_def, clarify) 
13145  834 
apply (erule_tac x = "[x]" in ballE) 
14208  835 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  836 
apply blast 
837 
done 

13114  838 

14339  839 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  840 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  841 

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

844 
apply(erule map_inj_on) 

845 
apply(blast intro:inj_onI dest:inj_onD) 

846 
done 

847 

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

13114  850 

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

851 
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

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

853 

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

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

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

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

857 

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

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

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

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

861 

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

862 

15392  863 
subsubsection {* @{text rev} *} 
13114  864 

13142  865 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  866 
by (induct xs) auto 
13114  867 

13142  868 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  869 
by (induct xs) auto 
13114  870 

15870  871 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
872 
by auto 

873 

13142  874 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  875 
by (induct xs) auto 
13114  876 

13142  877 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  878 
by (induct xs) auto 
13114  879 

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

882 

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

884 
by (cases xs) auto 

885 

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

886 
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

887 
apply (induct xs arbitrary: ys, force) 
14208  888 
apply (case_tac ys, simp, force) 
13145  889 
done 
13114  890 

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

893 

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

896 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  897 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
898 
done 

13114  899 

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

13145  902 
by (induct xs rule: rev_induct) auto 
13114  903 

13366  904 
lemmas rev_cases = rev_exhaust 
905 

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

908 

13114  909 

15392  910 
subsubsection {* @{text set} *} 
13114  911 

13142  912 
lemma finite_set [iff]: "finite (set xs)" 
13145  913 
by (induct xs) auto 
13114  914 

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

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

14099  920 

13142  921 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  922 
by auto 
13114  923 

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

926 

13142  927 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  928 
by (induct xs) auto 
13114  929 

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

932 

13142  933 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  934 
by (induct xs) auto 
13114  935 

13142  936 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  937 
by (induct xs) auto 
13114  938 

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

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

13114  944 

13142  945 

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

946 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  947 
proof (induct xs) 
26073  948 
case Nil thus ?case by simp 
949 
next 

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

951 
qed 

952 

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

26073  955 

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

957 
proof (induct xs) 

958 
case Nil thus ?case by simp 

18049  959 
next 
960 
case (Cons a xs) 

961 
show ?case 

962 
proof cases 

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

963 
assume "x = a" thus ?case using Cons by fastsimp 
18049  964 
next 
26073  965 
assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI) 
966 
qed 

967 
qed 

968 

969 
lemma in_set_conv_decomp_first: 

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

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

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

974 
proof (induct xs rule:rev_induct) 

975 
case Nil thus ?case by simp 

976 
next 

977 
case (snoc a xs) 

978 
show ?case 

979 
proof cases 

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

981 
next 

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

18049  983 
qed 
984 
qed 

985 

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

26734  988 
by (auto dest!: split_list_last) 
26073  989 

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

991 
proof (induct xs) 

992 
case Nil thus ?case by simp 

993 
next 

994 
case Cons thus ?case 

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

996 
qed 

997 

998 
lemma split_list_propE: 

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

1001 
using split_list_prop [OF assms] by blast 

26073  1002 

1003 
lemma split_list_first_prop: 

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

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

26734  1006 
proof (induct xs) 
26073  1007 
case Nil thus ?case by simp 
1008 
next 

1009 
case (Cons x xs) 

1010 
show ?case 

1011 
proof cases 

1012 
assume "P x" 

26734  1013 
thus ?thesis by simp 
1014 
(metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 

26073  1015 
next 
1016 
assume "\<not> P x" 

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

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

1019 
qed 

1020 
qed 

1021 

1022 
lemma split_list_first_propE: 

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

1025 
using split_list_first_prop [OF assms] by blast 

26073  1026 

1027 
lemma split_list_first_prop_iff: 

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

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

26734  1030 
by (rule, erule split_list_first_prop) auto 
26073  1031 

1032 
lemma split_list_last_prop: 

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

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

1035 
proof(induct xs rule:rev_induct) 

1036 
case Nil thus ?case by simp 

1037 
next 

1038 
case (snoc x xs) 

1039 
show ?case 

1040 
proof cases 

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

1042 
next 

1043 
assume "\<not> P x" 

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

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

1046 
qed 

1047 
qed 

1048 

1049 
lemma split_list_last_propE: 

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

1052 
using split_list_last_prop [OF assms] by blast 

26073  1053 

1054 
lemma split_list_last_prop_iff: 

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

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

26734  1057 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1058 

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

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

13508  1062 

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

13114  1065 

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

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

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

1068 
by (induct xs) auto 
15168  1069 

35115  1070 

15392  1071 
subsubsection {* @{text filter} *} 
13114  1072 

13142  1073 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1074 
by (induct xs) auto 
13114  1075 

15305  1076 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1077 
by (induct xs) simp_all 

1078 

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

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

1084 

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

1087 
by(induct xs) simp_all 

1088 

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

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

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

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

1099 
apply (induct xs) 

1100 
apply auto 

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

1102 
apply simp 

1103 
done 

13114  1104 

16965  1105 
lemma filter_map: 
1106 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1107 
by (induct xs) simp_all 

1108 

1109 
lemma length_filter_map[simp]: 

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

1111 
by (simp add:filter_map) 

1112 

13142  1113 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1114 
by auto 
13114  1115 

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

1118 
proof (induct xs) 

1119 
case Nil thus ?case by simp 

1120 
next 

1121 
case (Cons x xs) thus ?case 

1122 
apply (auto split:split_if_asm) 

1123 
using length_filter_le[of P xs] apply arith 

1124 
done 

1125 
qed 

13114  1126 

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

1129 
proof (induct xs) 

1130 
case Nil thus ?case by simp 

1131 
next 

1132 
case (Cons x xs) 

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

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

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

1136 
proof (cases) 

1137 
assume "p x" 

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

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

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

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

1146 
finally show ?thesis . 

1147 
next 

1148 
assume "\<not> p x" 

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

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

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

1156 
by (simp add:card_insert_if) 

1157 
finally show ?thesis . 

1158 
qed 

1159 
qed 

1160 

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

1163 
\<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  1164 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1165 
proof(induct ys) 
1166 
case Nil thus ?case by simp 

1167 
next 

1168 
case (Cons y ys) 

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

1170 
proof cases 

1171 
assume Py: "P y" 

1172 
show ?thesis 

1173 
proof cases 

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

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

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

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

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

1179 
with Py Cons.prems show ?thesis by simp 
17629  1180 
qed 
1181 
next 

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

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

1183 
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

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

1185 
then show ?thesis .. 
17629  1186 
qed 
1187 
qed 

1188 

1189 
lemma filter_eq_ConsD: 

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

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

1192 
by(rule Cons_eq_filterD) simp 

1193 

1194 
lemma filter_eq_Cons_iff: 

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

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

1197 
by(auto dest:filter_eq_ConsD) 

1198 

1199 
lemma Cons_eq_filter_iff: 

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

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

1202 
by(auto dest:Cons_eq_filterD) 

1203 

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

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

1207 
apply(erule thin_rl) 

1208 
by (induct ys) simp_all 

1209 

15281  1210 

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

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

1212 

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

1213 
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

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

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

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

1217 
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

1218 

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

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

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

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

1222 

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

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

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

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

1226 

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

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

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

1229 
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

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

1231 
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

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

1233 
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

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

1235 

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

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

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

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

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

1240 
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

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

1242 
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

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

1244 

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

1245 
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

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

1247 
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

1248 
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

1249 

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

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

1251 

35115  1252 

15392  1253 
subsubsection {* @{text concat} *} 
13114  1254 

13142  1255 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1256 
by (induct xs) auto 
13114  1257 

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

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

24308  1264 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1265 
by (induct xs) auto 
13114  1266 

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

1267 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1268 
by (induct xs) auto 
1269 

13142  1270 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1271 
by (induct xs) auto 
13114  1272 

13142  1273 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1274 
by (induct xs) auto 
13114  1275 

13142  1276 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1277 
by (induct xs) auto 
13114  1278 

1279 

15392  1280 
subsubsection {* @{text nth} *} 
13114  1281 

29827  1282 
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" 
13145  1283 
by auto 
13114  1284 

29827  1285 
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n" 
13145  1286 
by auto 
13114  1287 

13142  1288 
declare nth.simps [simp del] 
13114  1289 

1290 
lemma nth_append: 

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

14208  1293 
apply (case_tac n, auto) 
13145  1294 
done 
13114  1295 

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

1296 
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

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

1298 

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

1299 
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

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

1301 

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

14208  1304 
apply (case_tac n, auto) 
13145  1305 
done 
13114  1306 

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

1309 

18049  1310 

1311 
lemma list_eq_iff_nth_eq: 

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

24632  1314 
apply force 
18049  1315 
apply(case_tac ys) 
1316 
apply simp 

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

1318 
done 

1319 

13142  1320 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  1321 
apply (induct xs, simp, simp) 
13145  1322 
apply safe 
24632  1323 
apply (metis nat_case_0 nth.simps zero_less_Suc) 
1324 
apply (metis less_Suc_eq_0_disj nth_Cons_Suc) 

14208  1325 
apply (case_tac i, simp) 
24632  1326 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1327 
done 
13114  1328 

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

1331 

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

13114  1334 

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

1338 
lemma all_nth_imp_all_set: 
