author  hoelzl 
Thu, 12 Nov 2009 17:21:48 +0100  
changeset 33639  603320b93668 
parent 33593  ef54e2108b74 
child 33640  0d82107dc07a 
permissions  rwrr 
13462  1 
(* Title: HOL/List.thy 
2 
Author: Tobias Nipkow 

923  3 
*) 
4 

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

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

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

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

923  15 

15392  16 
subsection{*Basic list processing functions*} 
15302  17 

923  18 
consts 
13366  19 
filter:: "('a => bool) => 'a list => 'a list" 
20 
concat:: "'a list list => 'a list" 

21 
foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b" 

22 
foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b" 

23 
hd:: "'a list => 'a" 

24 
tl:: "'a list => 'a list" 

25 
last:: "'a list => 'a" 

26 
butlast :: "'a list => 'a list" 

27 
set :: "'a list => 'a set" 

28 
map :: "('a=>'b) => ('a list => 'b list)" 

23096  29 
listsum :: "'a list => 'a::monoid_add" 
13366  30 
list_update :: "'a list => nat => 'a => 'a list" 
31 
take:: "nat => 'a list => 'a list" 

32 
drop:: "nat => 'a list => 'a list" 

33 
takeWhile :: "('a => bool) => 'a list => 'a list" 

34 
dropWhile :: "('a => bool) => 'a list => 'a list" 

35 
rev :: "'a list => 'a list" 

36 
zip :: "'a list => 'b list => ('a * 'b) list" 

15425  37 
upt :: "nat => nat => nat list" ("(1[_..</_'])") 
13366  38 
remdups :: "'a list => 'a list" 
15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

39 
remove1 :: "'a => 'a list => 'a list" 
27693  40 
removeAll :: "'a => 'a list => 'a list" 
13366  41 
"distinct":: "'a list => bool" 
42 
replicate :: "nat => 'a => 'a list" 

19390  43 
splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
15302  44 

923  45 

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

47 

923  48 
syntax 
13366  49 
 {* list Enumeration *} 
50 
"@list" :: "args => 'a list" ("[(_)]") 

923  51 

13366  52 
 {* Special syntax for filter *} 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

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

13366  55 
 {* list update *} 
56 
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") 

57 
"" :: "lupdbind => lupdbinds" ("_") 

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

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

60 

923  61 
translations 
13366  62 
"[x, xs]" == "x#[xs]" 
63 
"[x]" == "x#[]" 

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

64 
"[x<xs . P]"== "filter (%x. P) xs" 
923  65 

13366  66 
"_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs" 
67 
"xs[i:=x]" == "list_update xs i x" 

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

68 

5427  69 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
10832
diff
changeset

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

71 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
14565  72 
syntax (HTML output) 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

73 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

74 

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

75 

13142  76 
text {* 
14589  77 
Function @{text size} is overloaded for all datatypes. Users may 
13366  78 
refer to the list version as @{text length}. *} 
13142  79 

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

81 
length :: "'a list => nat" where 
19363  82 
"length == size" 
15302  83 

5183  84 
primrec 
15307  85 
"hd(x#xs) = x" 
86 

5183  87 
primrec 
15307  88 
"tl([]) = []" 
89 
"tl(x#xs) = xs" 

90 

5183  91 
primrec 
15307  92 
"last(x#xs) = (if xs=[] then x else last xs)" 
93 

5183  94 
primrec 
15307  95 
"butlast []= []" 
96 
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" 

97 

5183  98 
primrec 
15307  99 
"set [] = {}" 
100 
"set (x#xs) = insert x (set xs)" 

101 

5183  102 
primrec 
15307  103 
"map f [] = []" 
104 
"map f (x#xs) = f(x)#map f xs" 

105 

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

106 
primrec 
25559  107 
append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) 
108 
where 

109 
append_Nil:"[] @ ys = ys" 

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

15307  111 

5183  112 
primrec 
15307  113 
"rev([]) = []" 
114 
"rev(x#xs) = rev(xs) @ [x]" 

115 

5183  116 
primrec 
15307  117 
"filter P [] = []" 
118 
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" 

119 

5183  120 
primrec 
15307  121 
foldl_Nil:"foldl f a [] = a" 
122 
foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" 

123 

8000  124 
primrec 
15307  125 
"foldr f [] a = a" 
126 
"foldr f (x#xs) a = f x (foldr f xs a)" 

127 

5183  128 
primrec 
15307  129 
"concat([]) = []" 
130 
"concat(x#xs) = x @ concat(xs)" 

131 

5183  132 
primrec 
23096  133 
"listsum [] = 0" 
134 
"listsum (x # xs) = x + listsum xs" 

135 

136 
primrec 

15307  137 
drop_Nil:"drop n [] = []" 
138 
drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs  Suc(m) => drop m xs)" 

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

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

141 

5183  142 
primrec 
15307  143 
take_Nil:"take n [] = []" 
144 
take_Cons: "take n (x#xs) = (case n of 0 => []  Suc(m) => x # take m xs)" 

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

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

147 

29822  148 
primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where 
149 
nth_Cons: "(x#xs)!n = (case n of 0 => x  (Suc k) => xs!k)" 

15307  150 
 {*Warning: simpset does not contain this definition, but separate 
151 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

152 

5183  153 
primrec 
15307  154 
"[][i:=v] = []" 
155 
"(x#xs)[i:=v] = (case i of 0 => v # xs  Suc j => x # xs[j:=v])" 

156 

157 
primrec 

158 
"takeWhile P [] = []" 

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

160 

5183  161 
primrec 
15307  162 
"dropWhile P [] = []" 
163 
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" 

164 

5183  165 
primrec 
15307  166 
"zip xs [] = []" 
167 
zip_Cons: "zip xs (y#ys) = (case xs of [] => []  z#zs => (z,y)#zip zs ys)" 

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

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

170 

5427  171 
primrec 
15425  172 
upt_0: "[i..<0] = []" 
173 
upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])" 

15307  174 

5183  175 
primrec 
15307  176 
"distinct [] = True" 
177 
"distinct (x#xs) = (x ~: set xs \<and> distinct xs)" 

178 

5183  179 
primrec 
15307  180 
"remdups [] = []" 
181 
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

182 

5183  183 
primrec 
15307  184 
"remove1 x [] = []" 
185 
"remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)" 

186 

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

187 
primrec 
27693  188 
"removeAll x [] = []" 
189 
"removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)" 

190 

191 
primrec 

15307  192 
replicate_0: "replicate 0 x = []" 
193 
replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

194 

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

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

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

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

198 

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

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

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

202 

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

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

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

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

207 

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

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

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

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

212 
primrec 

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

213 
"splice [] ys = ys" 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

214 
"splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))" 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

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

216 

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

219 
\fbox{ 

220 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

258 
\label{fig:Characteristic} 

259 
\end{figure} 

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

263 

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

266 

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

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

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

269 

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

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

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

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

275 
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

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

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

278 

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

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

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

281 
"sort_key f (x#xs) = insort_key f x (sort_key f xs)" 
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33593
diff
changeset

282 

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

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

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

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

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

287 

24616  288 

23388  289 
subsubsection {* List comprehension *} 
23192  290 

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

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

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

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

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

297 

298 
The qualifiers after the dot are 

299 
\begin{description} 

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

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

301 
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

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

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

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

306 
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

307 
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

308 
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

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

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

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

314 
definitions for the list comprehensions in question. *} 

315 

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

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

322 

23240  323 
nonterminals lc_qual lc_quals 
23192  324 

325 
syntax 

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

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

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

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

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

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

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

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

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

345 
*) 
23240  346 

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

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

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

352 
parse_translation (advanced) {* 

353 
let 

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

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

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

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

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

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

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

360 

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

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

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

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

367 
$ NilC; 
24349  368 
val cs = Syntax.const "_case2" $ case1 $ case2 
31784  369 
val ft = DatatypeCase.case_tr false Datatype.info_of_constr 
24349  370 
ctxt [x, cs] 
371 
in lambda x ft end; 

372 

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

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

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

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

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

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

380 
 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

381 

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

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

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

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

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

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

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

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

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

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

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

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

393 

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

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

396 

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

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

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

400 
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

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

402 
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

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

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

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

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

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

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

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

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

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

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

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

418 

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

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

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

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

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

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

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

432 

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

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

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

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

437 
append_eq_append_conv}. 
13142  438 
*} 
13114  439 

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

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

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

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

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

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

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

460 

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

13142  464 

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

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

470 

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

471 
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

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

473 

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

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

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

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

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

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

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

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

481 
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

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

483 

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

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

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

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

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

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

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

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

491 
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

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

493 
qed 
13114  494 

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

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

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

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

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

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

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

501 
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

502 

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

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

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

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

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

508 
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

509 
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

510 
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

511 
*) 
24037  512 

513 
let 

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

514 

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

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

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

519 
 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

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

521 

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

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

525 
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

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

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

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

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

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

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

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

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

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

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

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

542 

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

543 

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

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

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

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

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

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

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

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

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

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

13145  570 
done 
13142  571 

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

574 
apply (induct xs arbitrary: ys zs ts) 

14495  575 
apply fastsimp 
576 
apply(case_tac zs) 

577 
apply simp 

578 
apply fastsimp 

579 
done 

580 

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

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

13145  585 
by simp 
13114  586 

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

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

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

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

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

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

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

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

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

611 

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

614 
by(cases ys) auto 

615 

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

618 
by(cases ys) auto 

619 

14300  620 

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

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

13145  624 
by simp 
13114  625 

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

13114  629 

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

13114  633 

634 

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

638 
 both lists end in a singleton list, 

639 
 or both lists end in the same list. 

13142  640 
*} 
641 

26480  642 
ML {* 
3507  643 
local 
644 

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

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

13462  648 
 last t = t; 
13114  649 

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

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

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

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

13114  657 

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

16973  660 

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

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

664 
fun rearr conv = 

665 
let 

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

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

668 
val appT = [listT,listT] > listT 

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

671 
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

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

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

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

15531  679 
else NONE 
13462  680 
end; 
681 

13114  682 
in 
13462  683 

684 
val list_eq_simproc = 

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

13114  687 
end; 
688 

689 
Addsimprocs [list_eq_simproc]; 

690 
*} 

691 

692 

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

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

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

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

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

704 
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

705 
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

706 

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

707 
lemma map_compose: "map (f \<circ> g) xs = map f (map 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

708 
by simp 
13114  709 

13142  710 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  711 
by (induct xs) auto 
13114  712 

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

715 

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

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

13737  719 
by simp 
13114  720 

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

13142  724 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  725 
by (cases xs) auto 
13114  726 

18447  727 
lemma map_eq_Cons_conv: 
14025  728 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  729 
by (cases xs) auto 
13114  730 

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

734 

18447  735 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
736 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

737 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

738 

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

18447  741 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  742 

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

743 
lemma map_eq_imp_length_eq: 
26734  744 
assumes "map f xs = map f ys" 
745 
shows "length xs = length ys" 

746 
using assms proof (induct ys arbitrary: xs) 

747 
case Nil then show ?case by simp 

748 
next 

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

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

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

752 
with xs show ?case by simp 

753 
qed 

754 

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

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

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

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

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

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

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

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

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

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

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

765 

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

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

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

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

769 

13114  770 
lemma map_injective: 
24526  771 
"map f xs = map f ys ==> inj f ==> xs = ys" 
772 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  773 

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

776 

13114  777 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  778 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  779 

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

14208  781 
apply (unfold inj_on_def, clarify) 
13145  782 
apply (erule_tac x = "[x]" in ballE) 
14208  783 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  784 
apply blast 
785 
done 

13114  786 

14339  787 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  788 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  789 

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

792 
apply(erule map_inj_on) 

793 
apply(blast intro:inj_onI dest:inj_onD) 

794 
done 

795 

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

13114  798 

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

799 
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

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

801 

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

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

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

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

805 

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

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

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

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

809 

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

810 

15392  811 
subsubsection {* @{text rev} *} 
13114  812 

13142  813 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  814 
by (induct xs) auto 
13114  815 

13142  816 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  817 
by (induct xs) auto 
13114  818 

15870  819 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
820 
by auto 

821 

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

13142  825 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  826 
by (induct xs) auto 
13114  827 

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

830 

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

832 
by (cases xs) auto 

833 

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

834 
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

835 
apply (induct xs arbitrary: ys, force) 
14208  836 
apply (case_tac ys, simp, force) 
13145  837 
done 
13114  838 

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

841 

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

844 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  845 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
846 
done 

13114  847 

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

13145  850 
by (induct xs rule: rev_induct) auto 
13114  851 

13366  852 
lemmas rev_cases = rev_exhaust 
853 

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

856 

13114  857 

15392  858 
subsubsection {* @{text set} *} 
13114  859 

13142  860 
lemma finite_set [iff]: "finite (set xs)" 
13145  861 
by (induct xs) auto 
13114  862 

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

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

14099  868 

13142  869 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  870 
by auto 
13114  871 

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

874 

13142  875 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  876 
by (induct xs) auto 
13114  877 

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

880 

13142  881 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  882 
by (induct xs) auto 
13114  883 

13142  884 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  885 
by (induct xs) auto 
13114  886 

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

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

13114  892 

13142  893 

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

894 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  895 
proof (induct xs) 
26073  896 
case Nil thus ?case by simp 
897 
next 

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

899 
qed 

900 

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

26073  903 

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

905 
proof (induct xs) 

906 
case Nil thus ?case by simp 

18049  907 
next 
908 
case (Cons a xs) 

909 
show ?case 

910 
proof cases 

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

911 
assume "x = a" thus ?case using Cons by fastsimp 
18049  912 
next 
26073  913 
assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI) 
914 
qed 

915 
qed 

916 

917 
lemma in_set_conv_decomp_first: 

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

26734  919 
by (auto dest!: split_list_first) 
26073  920 

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

922 
proof (induct xs rule:rev_induct) 

923 
case Nil thus ?case by simp 

924 
next 

925 
case (snoc a xs) 

926 
show ?case 

927 
proof cases 

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

929 
next 

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

18049  931 
qed 
932 
qed 

933 

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

26734  936 
by (auto dest!: split_list_last) 
26073  937 

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

939 
proof (induct xs) 

940 
case Nil thus ?case by simp 

941 
next 

942 
case Cons thus ?case 

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

944 
qed 

945 

946 
lemma split_list_propE: 

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

949 
using split_list_prop [OF assms] by blast 

26073  950 

951 
lemma split_list_first_prop: 

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

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

26734  954 
proof (induct xs) 
26073  955 
case Nil thus ?case by simp 
956 
next 

957 
case (Cons x xs) 

958 
show ?case 

959 
proof cases 

960 
assume "P x" 

26734  961 
thus ?thesis by simp 
962 
(metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 

26073  963 
next 
964 
assume "\<not> P x" 

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

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

967 
qed 

968 
qed 

969 

970 
lemma split_list_first_propE: 

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

973 
using split_list_first_prop [OF assms] by blast 

26073  974 

975 
lemma split_list_first_prop_iff: 

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

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

26734  978 
by (rule, erule split_list_first_prop) auto 
26073  979 

980 
lemma split_list_last_prop: 

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

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

983 
proof(induct xs rule:rev_induct) 

984 
case Nil thus ?case by simp 

985 
next 

986 
case (snoc x xs) 

987 
show ?case 

988 
proof cases 

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

990 
next 

991 
assume "\<not> P x" 

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

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

994 
qed 

995 
qed 

996 

997 
lemma split_list_last_propE: 

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

1000 
using split_list_last_prop [OF assms] by blast 

26073  1001 

1002 
lemma split_list_last_prop_iff: 

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

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

26734  1005 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1006 

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

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

13508  1010 

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

13114  1013 

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

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

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

1016 
by (induct xs) auto 
15168  1017 

15392  1018 
subsubsection {* @{text filter} *} 
13114  1019 

13142  1020 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1021 
by (induct xs) auto 
13114  1022 

15305  1023 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1024 
by (induct xs) simp_all 

1025 

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

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

1031 

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

1034 
by(induct xs) simp_all 

1035 

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

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

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

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

1046 
apply (induct xs) 

1047 
apply auto 

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

1049 
apply simp 

1050 
done 

13114  1051 

16965  1052 
lemma filter_map: 
1053 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1054 
by (induct xs) simp_all 

1055 

1056 
lemma length_filter_map[simp]: 

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

1058 
by (simp add:filter_map) 

1059 

13142  1060 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1061 
by auto 
13114  1062 

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

1065 
proof (induct xs) 

1066 
case Nil thus ?case by simp 

1067 
next 

1068 
case (Cons x xs) thus ?case 

1069 
apply (auto split:split_if_asm) 

1070 
using length_filter_le[of P xs] apply arith 

1071 
done 

1072 
qed 

13114  1073 

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

1076 
proof (induct xs) 

1077 
case Nil thus ?case by simp 

1078 
next 

1079 
case (Cons x xs) 

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

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

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

1083 
proof (cases) 

1084 
assume "p x" 

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

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

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

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

1093 
finally show ?thesis . 

1094 
next 

1095 
assume "\<not> p x" 

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

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

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

1103 
by (simp add:card_insert_if) 

1104 
finally show ?thesis . 

1105 
qed 

1106 
qed 

1107 

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

1110 
\<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  1111 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1112 
proof(induct ys) 
1113 
case Nil thus ?case by simp 

1114 
next 

1115 
case (Cons y ys) 

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

1117 
proof cases 

1118 
assume Py: "P y" 

1119 
show ?thesis 

1120 
proof cases 

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

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

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

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

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

1126 
with Py Cons.prems show ?thesis by simp 
17629  1127 
qed 
1128 
next 

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

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

1130 
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

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

1132 
then show ?thesis .. 
17629  1133 
qed 
1134 
qed 

1135 

1136 
lemma filter_eq_ConsD: 

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

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

1139 
by(rule Cons_eq_filterD) simp 

1140 

1141 
lemma filter_eq_Cons_iff: 

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

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

1144 
by(auto dest:filter_eq_ConsD) 

1145 

1146 
lemma Cons_eq_filter_iff: 

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

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

1149 
by(auto dest:Cons_eq_filterD) 

1150 

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

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

1154 
apply(erule thin_rl) 

1155 
by (induct ys) simp_all 

1156 

15281  1157 

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

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

1159 

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

1160 
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

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

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

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

1164 
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

1165 

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

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

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

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

1169 

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

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

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

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

1173 

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

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

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

1176 
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

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

1178 
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

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

1180 
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

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

1182 

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

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

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

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

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

1187 
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

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

1189 
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

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

1191 

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

1192 
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

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

1194 
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

1195 
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

1196 

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

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

1198 

15392  1199 
subsubsection {* @{text concat} *} 
13114  1200 

13142  1201 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1202 
by (induct xs) auto 
13114  1203 

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

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

24308  1210 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1211 
by (induct xs) auto 
13114  1212 

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

1213 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1214 
by (induct xs) auto 
1215 

13142  1216 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1217 
by (induct xs) auto 
13114  1218 

13142  1219 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1220 
by (induct xs) auto 
13114  1221 

13142  1222 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1223 
by (induct xs) auto 
13114  1224 

1225 

15392  1226 
subsubsection {* @{text nth} *} 
13114  1227 

29827  1228 
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" 
13145  1229 
by auto 
13114  1230 

29827  1231 
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n" 
13145  1232 
by auto 
13114  1233 

13142  1234 
declare nth.simps [simp del] 
13114  1235 

1236 
lemma nth_append: 

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

14208  1239 
apply (case_tac n, auto) 
13145  1240 
done 
13114  1241 

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

1242 
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

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

1244 

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

1245 
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

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

1247 

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

14208  1250 
apply (case_tac n, auto) 
13145  1251 
done 
13114  1252 

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

1255 

18049  1256 

1257 
lemma list_eq_iff_nth_eq: 

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

24632  1260 
apply force 
18049  1261 
apply(case_tac ys) 
1262 
apply simp 

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

1264 
done 

1265 

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

14208  1271 
apply (case_tac i, simp) 
24632  1272 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1273 
done 
13114  1274 

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

1277 

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

13114  1280 

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

1284 
lemma all_nth_imp_all_set: 

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

13114  1287 

1288 
lemma all_set_conv_all_nth: 

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

13114  1291 

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

1294 
proof (induct xs arbitrary: n) 

1295 
case Nil thus ?case by simp 

1296 
next 

1297 
case (Cons x xs) 

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

1299 
moreover 

1300 
{ assume "n < length xs" 

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

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

1303 
moreover 

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

1305 
ultimately 

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

1307 
} 

1308 
ultimately 

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

1310 
qed 

13114  1311 

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

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

1315 
proof(induct k) 

1316 
case 0 show ?case by simp 

1317 
next 

1318 
case (Suc k) 

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

1320 
proof 

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

1322 
next 

1323 
assume "?L" 

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

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

1326 
thus "?R" .. 

1327 
qed 

1328 
qed 

1329 

1330 

15392  1331 
subsubsection {* @{text list_update} *} 
13114  1332 

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

13114  1335 

1336 
lemma nth_list_update: 

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

13114  1339 

13142  1340 
lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x" 
13145  1341 
by (simp add: nth_list_update) 
13114  1342 

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