author  nipkow 
Fri, 15 Feb 2008 17:36:21 +0100  
changeset 26073  0e70d3bd2eb4 
parent 25966  74f6817870f9 
child 26143  314c0bcb7df7 
permissions  rwrr 
13462  1 
(* Title: HOL/List.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

923  4 
*) 
5 

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

15131  8 
theory List 
25591
0792e02973cc
swtiched ATP_Linkup and PreList in theory hierarchy
haftmann
parents:
25571
diff
changeset

9 
imports ATP_Linkup 
21754
6316163ae934
moved char/string syntax to Tools/string_syntax.ML;
wenzelm
parents:
21548
diff
changeset

10 
uses "Tools/string_syntax.ML" 
15131  11 
begin 
923  12 

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

923  16 

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

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

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

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

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

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

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

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

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

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

23096  30 
listsum :: "'a list => 'a::monoid_add" 
13366  31 
nth :: "'a list => nat => 'a" (infixl "!" 100) 
32 
list_update :: "'a list => nat => 'a => 'a list" 

33 
take:: "nat => 'a list => 'a list" 

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

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

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

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

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

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

41 
remove1 :: "'a => 'a list => 'a list" 
13366  42 
"distinct":: "'a list => bool" 
43 
replicate :: "nat => 'a => 'a list" 

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

923  46 

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

48 

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

923  52 

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

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

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

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

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

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

61 

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

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

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

13366  67 
"_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs" 
68 
"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

69 

5427  70 

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

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

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

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

75 

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

76 

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

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

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

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

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

91 

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

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

98 

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

102 

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

106 

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

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

110 
append_Nil:"[] @ ys = ys" 

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

15307  112 

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

116 

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

120 

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

124 

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

128 

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

132 

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

136 

137 
primrec 

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

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

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

142 

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

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

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

148 

13142  149 
primrec 
15307  150 
nth_Cons:"(x#xs)!n = (case n of 0 => x  (Suc k) => xs!k)" 
151 
 {*Warning: simpset does not contain this definition, but separate 

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

153 

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

157 

158 
primrec 

159 
"takeWhile P [] = []" 

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

161 

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

165 

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

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

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

171 

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

15307  175 

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

179 

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

183 

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

187 

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

188 
primrec 
15307  189 
replicate_0: "replicate 0 x = []" 
190 
replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

191 

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

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

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

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

195 

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

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

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

198 
"rotate n = rotate1 ^ n" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

199 

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

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

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

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

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 
sublist :: "'a list => nat set => 'a list" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

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

209 
primrec 

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

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

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

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

213 

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

216 

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

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

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

219 

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

220 
fun sorted :: "'a list \<Rightarrow> bool" where 
24697  221 
"sorted [] \<longleftrightarrow> True"  
222 
"sorted [x] \<longleftrightarrow> True"  

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

25559  225 
primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
24697  226 
"insort x [] = [x]"  
25062  227 
"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))" 
24697  228 

25559  229 
primrec sort :: "'a list \<Rightarrow> 'a list" where 
24697  230 
"sort [] = []"  
231 
"sort (x#xs) = insort x (sort xs)" 

24616  232 

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

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

234 

24616  235 

23388  236 
subsubsection {* List comprehension *} 
23192  237 

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

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

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

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

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

244 

245 
The qualifiers after the dot are 

246 
\begin{description} 

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

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

248 
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

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

250 
%\item[local bindings] @ {text"let x = e"}. 
24349  251 
\end{description} 
23240  252 

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

253 
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

254 
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

255 
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

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

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

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

261 
definitions for the list comprehensions in question. *} 

262 

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

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

269 

23240  270 
nonterminals lc_qual lc_quals 
23192  271 

272 
syntax 

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

276 
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*) 
23240  277 
"_lc_end" :: "lc_quals" ("]") 
278 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 

24349  279 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  280 

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

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

282 
translation of [e. p<xs] 
23192  283 
translations 
24349  284 
"[e. p<xs]" => "concat(map (_lc_abs p [e]) xs)" 
23240  285 
"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" 
24349  286 
=> "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)" 
23240  287 
"[e. P]" => "if P then [e] else []" 
288 
"_listcompr e (_lc_test P) (_lc_quals Q Qs)" 

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

24349  290 
"_listcompr e (_lc_let b) (_lc_quals Q Qs)" 
291 
=> "_Let b (_listcompr e Q Qs)" 

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

292 
*) 
23240  293 

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

294 
syntax (xsymbols) 
24349  295 
"_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

296 
syntax (HTML output) 
24349  297 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
298 

299 
parse_translation (advanced) {* 

300 
let 

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

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

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

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

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

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

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

307 

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

308 
fun pat_tr ctxt p e opti = (* %x. case x of p => e  _ => [] *) 
24349  309 
let 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

310 
val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT); 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

311 
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

312 
val case1 = Syntax.const "_case1" $ p $ e; 
24349  313 
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

314 
$ NilC; 
24349  315 
val cs = Syntax.const "_case2" $ case1 $ case2 
316 
val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr 

317 
ctxt [x, cs] 

318 
in lambda x ft end; 

319 

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

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

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

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

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

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

327 
 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

328 

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

329 
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

330 
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

331 
 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

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

333 
 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

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

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

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

337 
 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

338 
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

339 
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

340 

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

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

343 

23240  344 
(* 
345 
term "[(x,y,z). b]" 

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

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

347 
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

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

349 
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

350 
term "[(x,y,z). x<a, x\<leftarrow>xs]" 
24349  351 
term "[(x,y). Cons True x \<leftarrow> xs]" 
352 
term "[(x,y,z). Cons x [] \<leftarrow> xs]" 

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

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

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

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

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

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

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

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

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

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

365 

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

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

367 
"xs \<noteq> x # xs" 
13145  368 
by (induct xs) auto 
13114  369 

13142  370 
lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] 
13114  371 

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

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

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

379 

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

380 
subsubsection {* @{const length} *} 
13114  381 

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

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

384 
append_eq_append_conv}. 
13142  385 
*} 
13114  386 

13142  387 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  388 
by (induct xs) auto 
13114  389 

13142  390 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  391 
by (induct xs) auto 
13114  392 

13142  393 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  394 
by (induct xs) auto 
13114  395 

13142  396 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  397 
by (cases xs) auto 
13114  398 

13142  399 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  400 
by (induct xs) auto 
13114  401 

13142  402 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  403 
by (induct xs) auto 
13114  404 

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

407 

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

13142  411 

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

14208  414 
apply (induct xs, simp, simp) 
14025  415 
apply blast 
416 
done 

417 

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

418 
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

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

420 

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

421 
lemma list_induct2 [consumes 1]: 
24526  422 
"\<lbrakk> length xs = length ys; 
14247  423 
P [] []; 
424 
\<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk> 

425 
\<Longrightarrow> P xs ys" 

24526  426 
apply(induct xs arbitrary: ys) 
14247  427 
apply simp 
428 
apply(case_tac ys) 

429 
apply simp 

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

430 
apply simp 
14247  431 
done 
13114  432 

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

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

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

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

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

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

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

439 
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

440 

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

441 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  442 
by (rule Eq_FalseI) auto 
24037  443 

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

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

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

446 
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

447 
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

448 
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

449 
*) 
24037  450 

451 
let 

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

452 

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

453 
fun len (Const("List.list.Nil",_)) acc = acc 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

454 
 len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1) 
23029  455 
 len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc) 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

456 
 len (Const("List.rev",_) $ xs) acc = len xs acc 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

457 
 len (Const("List.map",_) $ _ $ xs) acc = len xs acc 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

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

459 

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

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

463 
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

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

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

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

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

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

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

473 
in 
23214  474 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
475 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

480 

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

481 

15392  482 
subsubsection {* @{text "@"}  append *} 
13114  483 

13142  484 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  485 
by (induct xs) auto 
13114  486 

13142  487 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  488 
by (induct xs) auto 
3507  489 

24449  490 
interpretation semigroup_append: semigroup_add ["op @"] 
491 
by unfold_locales simp 

492 
interpretation monoid_append: monoid_add ["[]" "op @"] 

493 
by unfold_locales (simp+) 

494 

13142  495 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  496 
by (induct xs) auto 
13114  497 

13142  498 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  499 
by (induct xs) auto 
13114  500 

13142  501 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  502 
by (induct xs) auto 
13114  503 

13142  504 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  505 
by (induct xs) auto 
13114  506 

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

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

509 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  510 
apply (induct xs arbitrary: ys) 
14208  511 
apply (case_tac ys, simp, force) 
512 
apply (case_tac ys, force, simp) 

13145  513 
done 
13142  514 

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

517 
apply (induct xs arbitrary: ys zs ts) 

14495  518 
apply fastsimp 
519 
apply(case_tac zs) 

520 
apply simp 

521 
apply fastsimp 

522 
done 

523 

13142  524 
lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  525 
by simp 
13142  526 

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

13145  528 
by simp 
13114  529 

13142  530 
lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  531 
by simp 
13114  532 

13142  533 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  534 
using append_same_eq [of _ _ "[]"] by auto 
3507  535 

13142  536 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  537 
using append_same_eq [of "[]"] by auto 
13114  538 

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

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

13142  542 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  543 
by (induct xs) auto 
13114  544 

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

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

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

554 

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

557 
by(cases ys) auto 

558 

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

561 
by(cases ys) auto 

562 

14300  563 

13142  564 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  565 

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

13145  567 
by simp 
13114  568 

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

13114  572 

13142  573 
lemma append_eq_appendI: 
13145  574 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
575 
by (drule sym) simp 

13114  576 

577 

13142  578 
text {* 
13145  579 
Simplification procedure for all list equalities. 
580 
Currently only tries to rearrange @{text "@"} to see if 

581 
 both lists end in a singleton list, 

582 
 or both lists end in the same list. 

13142  583 
*} 
584 

585 
ML_setup {* 

3507  586 
local 
587 

13114  588 
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) = 
13462  589 
(case xs of Const("List.list.Nil",_) => cons  _ => last xs) 
23029  590 
 last (Const("List.append",_) $ _ $ ys) = last ys 
13462  591 
 last t = t; 
13114  592 

593 
fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true 

13462  594 
 list1 _ = false; 
13114  595 

596 
fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) = 

13462  597 
(case xs of Const("List.list.Nil",_) => xs  _ => cons $ butlast xs) 
23029  598 
 butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys 
13462  599 
 butlast xs = Const("List.list.Nil",fastype_of xs); 
13114  600 

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

16973  603 

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

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

607 
fun rearr conv = 

608 
let 

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

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

611 
val appT = [listT,listT] > listT 

23029  612 
val app = Const("List.append",appT) 
13462  613 
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

614 
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

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

616 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  617 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  618 

13462  619 
in 
22633  620 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
621 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  622 
else NONE 
13462  623 
end; 
624 

13114  625 
in 
13462  626 

627 
val list_eq_simproc = 

22633  628 
Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq); 
13462  629 

13114  630 
end; 
631 

632 
Addsimprocs [list_eq_simproc]; 

633 
*} 

634 

635 

15392  636 
subsubsection {* @{text map} *} 
13114  637 

13142  638 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  639 
by (induct xs) simp_all 
13114  640 

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

13142  644 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  645 
by (induct xs) auto 
13114  646 

13142  647 
lemma map_compose: "map (f o g) xs = map f (map g xs)" 
13145  648 
by (induct xs) (auto simp add: o_def) 
13114  649 

13142  650 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  651 
by (induct xs) auto 
13114  652 

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

655 

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

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

13737  659 
by simp 
13114  660 

13142  661 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  662 
by (cases xs) auto 
13114  663 

13142  664 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  665 
by (cases xs) auto 
13114  666 

18447  667 
lemma map_eq_Cons_conv: 
14025  668 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  669 
by (cases xs) auto 
13114  670 

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

674 

18447  675 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
676 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

677 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

678 

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

18447  681 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  682 

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

683 
lemma map_eq_imp_length_eq: 
24526  684 
"map f xs = map f ys ==> length xs = length ys" 
685 
apply (induct ys arbitrary: xs) 

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

686 
apply simp 
24632  687 
apply (metis Suc_length_conv length_map) 
15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

689 

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

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

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

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

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

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

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

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

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

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

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

700 

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

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

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

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

704 

13114  705 
lemma map_injective: 
24526  706 
"map f xs = map f ys ==> inj f ==> xs = ys" 
707 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  708 

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

711 

13114  712 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  713 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  714 

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

14208  716 
apply (unfold inj_on_def, clarify) 
13145  717 
apply (erule_tac x = "[x]" in ballE) 
14208  718 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  719 
apply blast 
720 
done 

13114  721 

14339  722 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  723 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  724 

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

727 
apply(erule map_inj_on) 

728 
apply(blast intro:inj_onI dest:inj_onD) 

729 
done 

730 

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

13114  733 

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

734 
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

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

736 

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

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

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

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

740 

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

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

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

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

744 

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

745 

15392  746 
subsubsection {* @{text rev} *} 
13114  747 

13142  748 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  749 
by (induct xs) auto 
13114  750 

13142  751 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  752 
by (induct xs) auto 
13114  753 

15870  754 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
755 
by auto 

756 

13142  757 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  758 
by (induct xs) auto 
13114  759 

13142  760 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  761 
by (induct xs) auto 
13114  762 

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

765 

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

767 
by (cases xs) auto 

768 

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

769 
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

770 
apply (induct xs arbitrary: ys, force) 
14208  771 
apply (case_tac ys, simp, force) 
13145  772 
done 
13114  773 

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

776 

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

779 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  780 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
781 
done 

13114  782 

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

13145  785 
by (induct xs rule: rev_induct) auto 
13114  786 

13366  787 
lemmas rev_cases = rev_exhaust 
788 

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

791 

13114  792 

15392  793 
subsubsection {* @{text set} *} 
13114  794 

13142  795 
lemma finite_set [iff]: "finite (set xs)" 
13145  796 
by (induct xs) auto 
13114  797 

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

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

14099  803 

13142  804 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  805 
by auto 
13114  806 

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

809 

13142  810 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  811 
by (induct xs) auto 
13114  812 

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

815 

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

13142  819 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  820 
by (induct xs) auto 
13114  821 

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

15425  825 
lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}" 
14208  826 
apply (induct j, simp_all) 
827 
apply (erule ssubst, auto) 

13145  828 
done 
13114  829 

13142  830 

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

831 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  832 
proof (induct xs) 
26073  833 
case Nil thus ?case by simp 
834 
next 

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

836 
qed 

837 

838 
lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)" 

839 
by (metis Un_upper2 insert_subset set.simps(2) set_append split_list) 

840 

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

842 
proof (induct xs) 

843 
case Nil thus ?case by simp 

18049  844 
next 
845 
case (Cons a xs) 

846 
show ?case 

847 
proof cases 

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

848 
assume "x = a" thus ?case using Cons by fastsimp 
18049  849 
next 
26073  850 
assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI) 
851 
qed 

852 
qed 

853 

854 
lemma in_set_conv_decomp_first: 

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

856 
by (metis in_set_conv_decomp split_list_first) 

857 

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

859 
proof (induct xs rule:rev_induct) 

860 
case Nil thus ?case by simp 

861 
next 

862 
case (snoc a xs) 

863 
show ?case 

864 
proof cases 

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

866 
next 

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

18049  868 
qed 
869 
qed 

870 

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

873 
by (metis in_set_conv_decomp split_list_last) 

874 

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

876 
proof (induct xs) 

877 
case Nil thus ?case by simp 

878 
next 

879 
case Cons thus ?case 

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

881 
qed 

882 

883 
lemma split_list_propE: 

884 
assumes "\<exists>x \<in> set xs. P x" 

885 
obtains ys x zs where "xs = ys @ x # zs" and "P x" 

886 
by(metis split_list_prop[OF assms]) 

887 

888 

889 
lemma split_list_first_prop: 

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

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

892 
proof(induct xs) 

893 
case Nil thus ?case by simp 

894 
next 

895 
case (Cons x xs) 

896 
show ?case 

897 
proof cases 

898 
assume "P x" 

899 
thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 

900 
next 

901 
assume "\<not> P x" 

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

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

904 
qed 

905 
qed 

906 

907 
lemma split_list_first_propE: 

908 
assumes "\<exists>x \<in> set xs. P x" 

909 
obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y" 

910 
by(metis split_list_first_prop[OF assms]) 

911 

912 
lemma split_list_first_prop_iff: 

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

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

915 
by(metis split_list_first_prop[where P=P] in_set_conv_decomp) 

916 

917 

918 
lemma split_list_last_prop: 

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

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

921 
proof(induct xs rule:rev_induct) 

922 
case Nil thus ?case by simp 

923 
next 

924 
case (snoc x xs) 

925 
show ?case 

926 
proof cases 

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

928 
next 

929 
assume "\<not> P x" 

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

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

932 
qed 

933 
qed 

934 

935 
lemma split_list_last_propE: 

936 
assumes "\<exists>x \<in> set xs. P x" 

937 
obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z" 

938 
by(metis split_list_last_prop[OF assms]) 

939 

940 
lemma split_list_last_prop_iff: 

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

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

943 
by(metis split_list_last_prop[where P=P] in_set_conv_decomp) 

944 

945 

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

13508  947 
apply (erule finite_induct, auto) 
26073  948 
apply (metis set.simps(2)) 
13508  949 
done 
950 

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

13114  953 

15168  954 

15392  955 
subsubsection {* @{text filter} *} 
13114  956 

13142  957 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  958 
by (induct xs) auto 
13114  959 

15305  960 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
961 
by (induct xs) simp_all 

962 

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

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

968 

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

971 
by(induct xs) simp_all 

972 

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

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

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

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

983 
apply (induct xs) 

984 
apply auto 

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

986 
apply simp 

987 
done 

13114  988 

16965  989 
lemma filter_map: 
990 
"filter P (map f xs) = map f (filter (P o f) xs)" 

991 
by (induct xs) simp_all 

992 

993 
lemma length_filter_map[simp]: 

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

995 
by (simp add:filter_map) 

996 

13142  997 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  998 
by auto 
13114  999 

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

1002 
proof (induct xs) 

1003 
case Nil thus ?case by simp 

1004 
next 

1005 
case (Cons x xs) thus ?case 

1006 
apply (auto split:split_if_asm) 

1007 
using length_filter_le[of P xs] apply arith 

1008 
done 

1009 
qed 

13114  1010 

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

1013 
proof (induct xs) 

1014 
case Nil thus ?case by simp 

1015 
next 

1016 
case (Cons x xs) 

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

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

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

1020 
proof (cases) 

1021 
assume "p x" 

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

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

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

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

1030 
finally show ?thesis . 

1031 
next 

1032 
assume "\<not> p x" 

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

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

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

1040 
by (simp add:card_insert_if) 

1041 
finally show ?thesis . 

1042 
qed 

1043 
qed 

1044 

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

1047 
\<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  1048 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1049 
proof(induct ys) 
1050 
case Nil thus ?case by simp 

1051 
next 

1052 
case (Cons y ys) 

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

1054 
proof cases 

1055 
assume Py: "P y" 

1056 
show ?thesis 

1057 
proof cases 

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

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

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

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

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

1063 
with Py Cons.prems show ?thesis by simp 
17629  1064 
qed 
1065 
next 

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

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

1067 
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

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

1069 
then show ?thesis .. 
17629  1070 
qed 
1071 
qed 

1072 

1073 
lemma filter_eq_ConsD: 

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

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

1076 
by(rule Cons_eq_filterD) simp 

1077 

1078 
lemma filter_eq_Cons_iff: 

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

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

1081 
by(auto dest:filter_eq_ConsD) 

1082 

1083 
lemma Cons_eq_filter_iff: 

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

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

1086 
by(auto dest:Cons_eq_filterD) 

1087 

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

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

1091 
apply(erule thin_rl) 

1092 
by (induct ys) simp_all 

1093 

15281  1094 

15392  1095 
subsubsection {* @{text concat} *} 
13114  1096 

13142  1097 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1098 
by (induct xs) auto 
13114  1099 

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

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

24308  1106 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1107 
by (induct xs) auto 
13114  1108 

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

1109 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1110 
by (induct xs) auto 
1111 

13142  1112 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1113 
by (induct xs) auto 
13114  1114 

13142  1115 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1116 
by (induct xs) auto 
13114  1117 

13142  1118 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1119 
by (induct xs) auto 
13114  1120 

1121 

15392  1122 
subsubsection {* @{text nth} *} 
13114  1123 

13142  1124 
lemma nth_Cons_0 [simp]: "(x # xs)!0 = x" 
13145  1125 
by auto 
13114  1126 

13142  1127 
lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n" 
13145  1128 
by auto 
13114  1129 

13142  1130 
declare nth.simps [simp del] 
13114  1131 

1132 
lemma nth_append: 

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

14208  1135 
apply (case_tac n, auto) 
13145  1136 
done 
13114  1137 

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

1138 
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

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

1140 

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

1141 
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

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

1143 

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

14208  1146 
apply (case_tac n, auto) 
13145  1147 
done 
13114  1148 

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

1151 

18049  1152 

1153 
lemma list_eq_iff_nth_eq: 

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

24632  1156 
apply force 
18049  1157 
apply(case_tac ys) 
1158 
apply simp 

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

1160 
done 

1161 

13142  1162 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  1163 
apply (induct xs, simp, simp) 
13145  1164 
apply safe 
24632  1165 
apply (metis nat_case_0 nth.simps zero_less_Suc) 
1166 
apply (metis less_Suc_eq_0_disj nth_Cons_Suc) 

14208  1167 
apply (case_tac i, simp) 
24632  1168 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1169 
done 
13114  1170 

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

1173 

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

13114  1176 

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

1180 
lemma all_nth_imp_all_set: 

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

13114  1183 

1184 
lemma all_set_conv_all_nth: 

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

13114  1187 

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

1190 
proof (induct xs arbitrary: n) 

1191 
case Nil thus ?case by simp 

1192 
next 

1193 
case (Cons x xs) 

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

1195 
moreover 

1196 
{ assume "n < length xs" 

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

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

1199 
moreover 

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

1201 
ultimately 

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

1203 
} 

1204 
ultimately 

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

1206 
qed 

13114  1207 

15392  1208 
subsubsection {* @{text list_update} *} 
13114  1209 

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

13114  1212 

1213 
lemma nth_list_update: 

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

13114  1216 

13142  1217 
lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x" 
13145  1218 
by (simp add: nth_list_update) 
13114  1219 

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

13114  1222 

13142  1223 
lemma list_update_overwrite [simp]: 
24526  1224 
"i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]" 
1225 
by (induct xs arbitrary: i) (auto split: nat.split) 

1226 

1227 
lemma list_update_id[simp]: "xs[i := xs!i] = xs" 

1228 
by (induct xs arbitrary: i) (simp_all split:nat.splits) 

1229 

1230 
lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs" 

1231 
apply (induct xs arbitrary: i) 

17501  1232 
apply simp 
1233 
apply (case_tac i) 

1234 
apply simp_all 

1235 
done 

1236 

13114  1237 
lemma list_update_same_conv: 
24526  1238 
"i < length xs ==> (xs[i := x] = xs) = (xs!i = x)" 
1239 
by (induct xs arbitrary: i) (auto split: nat.split) 

13114  1240 

14187  1241 
lemma list_update_append1: 
24526  1242 
"i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys" 
1243 
apply (induct xs arbitrary: i, simp) 

14187  1244 
apply(simp split:nat.split) 
1245 
done 

1246 

15868  1247 
lemma list_update_append: 
24526  1248 
"(xs @ ys) [n:= x] = 
15868  1249 
(if n < length xs then xs[n:= x] @ ys else xs @ (ys [nlength xs:= x]))" 
24526  1250 
by (induct xs arbitrary: n) (auto split:nat.splits) 
15868  1251 

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

1252 
lemma list_update_length [simp]: 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1253 
"(xs @ x # ys)[length xs := y] = (xs @ y # ys)" 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

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

1255 

13114  1256 
lemma update_zip: 
24526  1257 
"length xs = length ys ==> 
1258 
(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])" 

1259 
by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split) 

1260 

1261 
lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)" 

1262 
by (induct xs arbitrary: i) (auto split: nat.split) 

13114  1263 

1264 
lemma set_update_subsetI: "[ set xs <= A; x:A ] ==> set(xs[i := x]) <= A" 

13145  1265 
by (blast dest!: set_update_subset_insert [THEN subsetD]) 
13114  1266 

24526  1267 
lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])" 
1268 
by (induct xs arbitrary: n) (auto split:nat.splits) 

15868  1269 

24796  1270 
lemma list_update_overwrite: 
1271 
"xs [i := x, i := y] = xs [i := y]" 

1272 
apply (induct xs arbitrary: i) 

1273 
apply simp 

1274 
apply (case_tac i) 

1275 
apply simp_all 

1276 
done 

1277 

1278 
lemma list_update_swap: 

1279 
"i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]" 

1280 
apply (induct xs arbitrary: i i') 

1281 
apply simp 

1282 
apply (case_tac i, case_tac i') 

1283 
apply auto 

1284 
apply (case_tac i') 

1285 
apply auto 

1286 
done 

1287 

13114  1288 

15392  1289 
subsubsection {* @{text last} and @{text butlast} *} 
13114  1290 

13142  1291 
lemma last_snoc [simp]: "last (xs @ [x]) = x" 
13145  1292 
by (induct xs) auto 
13114  1293 

13142  1294 
lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs" 
13145  1295 
by (induct xs) auto 
13114  1296 

14302  1297 
lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x" 
1298 
by(simp add:last.simps) 

1299 

1300 
lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs" 

1301 
by(simp add:last.simps) 

1302 

1303 
lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)" 

1304 
by (induct xs) (auto) 

1305 

1306 
lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs" 

1307 
by(simp add:last_append) 

1308 

1309 
lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys" 

1310 
by(simp add:last_append) 

1311 

17762  1312 
lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs" 
1313 
by(rule rev_exhaust[of xs]) simp_all 

1314 

1315 
lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs" 

1316 
by(cases xs) simp_all 

1317 

17765  1318 
lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as" 
1319 
by (induct as) auto 

17762  1320 

13142  1321 
lemma length_butlast [simp]: "length (butlast xs) = length xs  1" 
13145  1322 
by (induct xs rule: rev_induct) auto 
13114  1323 

1324 
lemma butlast_append: 

24526  1325 
"butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)" 
1326 
by (induct xs arbitrary: ys) auto 

13114  1327 

13142  1328 
lemma append_butlast_last_id [simp]: 
13145  1329 
"xs \<noteq> [] ==> butlast xs @ [last xs] = xs" 
1330 
by (induct xs) auto 

13114  1331 

13142  1332 
lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs" 
13145  1333 
by (induct xs) (auto split: split_if_asm) 
13114  1334 

1335 
lemma in_set_butlast_appendI: 

13145  1336 
"x : set (butlast xs)  x : set (butlast ys) ==> x : set (butlast (xs @ ys))" 
1337 
by (auto dest: in_set_butlastD simp add: butlast_append) 

13114  1338 

24526  1339 
lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs" 
1340 
apply (induct xs arbitrary: n) 

17501  1341 
apply simp 
1342 
apply (auto split:nat.split) 

1343 
done 

1344 

17589  1345 
lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs  1)" 
1346 
by(induct xs)(auto simp:neq_Nil_conv) 

1347 