author  blanchet 
Thu, 01 Sep 2011 13:18:27 +0200  
changeset 44635  3d046864ebe6 
parent 44619  fd520fa2fb09 
child 44890  22f665a2e91c 
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 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
43594
diff
changeset

8 
imports Plain Presburger Code_Numeral Quotient ATP 
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

9 
uses 
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

10 
("Tools/list_code.ML") 
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

11 
("Tools/list_to_set_comprehension.ML") 
15131  12 
begin 
923  13 

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

923  17 

34941  18 
syntax 
19 
 {* list Enumeration *} 

35115  20 
"_list" :: "args => 'a list" ("[(_)]") 
34941  21 

22 
translations 

23 
"[x, xs]" == "x#[xs]" 

24 
"[x]" == "x#[]" 

25 

35115  26 

27 
subsection {* Basic list processing functions *} 

15302  28 

34941  29 
primrec 
30 
hd :: "'a list \<Rightarrow> 'a" where 

31 
"hd (x # xs) = x" 

32 

33 
primrec 

34 
tl :: "'a list \<Rightarrow> 'a list" where 

35 
"tl [] = []" 

36 
 "tl (x # xs) = xs" 

37 

38 
primrec 

39 
last :: "'a list \<Rightarrow> 'a" where 

40 
"last (x # xs) = (if xs = [] then x else last xs)" 

41 

42 
primrec 

43 
butlast :: "'a list \<Rightarrow> 'a list" where 

44 
"butlast []= []" 

45 
 "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)" 

46 

47 
primrec 

48 
set :: "'a list \<Rightarrow> 'a set" where 

49 
"set [] = {}" 

50 
 "set (x # xs) = insert x (set xs)" 

51 

52 
primrec 

53 
map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where 

54 
"map f [] = []" 

55 
 "map f (x # xs) = f x # map f xs" 

56 

57 
primrec 

58 
append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where 

59 
append_Nil:"[] @ ys = ys" 

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

61 

62 
primrec 

63 
rev :: "'a list \<Rightarrow> 'a list" where 

64 
"rev [] = []" 

65 
 "rev (x # xs) = rev xs @ [x]" 

66 

67 
primrec 

68 
filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

69 
"filter P [] = []" 

70 
 "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)" 

71 

72 
syntax 

73 
 {* Special syntax for filter *} 

35115  74 
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<_./ _])") 
34941  75 

76 
translations 

77 
"[x<xs . P]"== "CONST filter (%x. P) xs" 

78 

79 
syntax (xsymbols) 

35115  80 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  81 
syntax (HTML output) 
35115  82 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  83 

84 
primrec 

85 
foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where 

86 
foldl_Nil: "foldl f a [] = a" 

87 
 foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs" 

88 

89 
primrec 

90 
foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where 

91 
"foldr f [] a = a" 

92 
 "foldr f (x # xs) a = f x (foldr f xs a)" 

93 

94 
primrec 

95 
concat:: "'a list list \<Rightarrow> 'a list" where 

96 
"concat [] = []" 

97 
 "concat (x # xs) = x @ concat xs" 

98 

39774  99 
definition (in monoid_add) 
34941  100 
listsum :: "'a list \<Rightarrow> 'a" where 
39774  101 
"listsum xs = foldr plus xs 0" 
34941  102 

103 
primrec 

104 
drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

105 
drop_Nil: "drop n [] = []" 

106 
 drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs  Suc m \<Rightarrow> drop m xs)" 

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

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

109 

110 
primrec 

111 
take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

112 
take_Nil:"take n [] = []" 

113 
 take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> []  Suc m \<Rightarrow> x # take m xs)" 

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

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

116 

117 
primrec 

118 
nth :: "'a list => nat => 'a" (infixl "!" 100) where 

119 
nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x  Suc k \<Rightarrow> xs ! k)" 

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

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

122 

123 
primrec 

124 
list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 

125 
"list_update [] i v = []" 

126 
 "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs  Suc j \<Rightarrow> x # list_update xs j v)" 

923  127 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
41075
diff
changeset

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

129 

923  130 
syntax 
13366  131 
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") 
132 
"" :: "lupdbind => lupdbinds" ("_") 

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

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

135 

923  136 
translations 
35115  137 
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" 
34941  138 
"xs[i:=x]" == "CONST list_update xs i x" 
139 

140 
primrec 

141 
takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

142 
"takeWhile P [] = []" 

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

144 

145 
primrec 

146 
dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

147 
"dropWhile P [] = []" 

148 
 "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)" 

149 

150 
primrec 

151 
zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where 

152 
"zip xs [] = []" 

153 
 zip_Cons: "zip xs (y # ys) = (case xs of [] => []  z # zs => (z, y) # zip zs ys)" 

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

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

156 

157 
primrec 

158 
upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where 

159 
upt_0: "[i..<0] = []" 

160 
 upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])" 

161 

34978
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

162 
definition 
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

163 
insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

164 
"insert x xs = (if x \<in> set xs then xs else x # xs)" 
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

165 

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

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

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

168 

34941  169 
primrec 
170 
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

171 
"remove1 x [] = []" 

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

173 

174 
primrec 

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

176 
"removeAll x [] = []" 

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

178 

40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

179 
primrec 
39915
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

180 
distinct :: "'a list \<Rightarrow> bool" where 
40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

181 
"distinct [] \<longleftrightarrow> True" 
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

182 
 "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs" 
39915
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

183 

ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

184 
primrec 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

185 
remdups :: "'a list \<Rightarrow> 'a list" where 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

186 
"remdups [] = []" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

187 
 "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

188 

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

191 
replicate_0: "replicate 0 x = []" 

192 
 replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

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

193 

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

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

15307  201 

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

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

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

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

205 

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

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

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

209 

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

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

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

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

214 

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

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

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

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

40593
1e57b18d27b1
code eqn for slice was missing; redefined splice with fun
nipkow
parents:
40365
diff
changeset

219 
fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
1e57b18d27b1
code eqn for slice was missing; redefined splice with fun
nipkow
parents:
40365
diff
changeset

220 
"splice [] ys = ys"  
1e57b18d27b1
code eqn for slice was missing; redefined splice with fun
nipkow
parents:
40365
diff
changeset

221 
"splice xs [] = xs"  
1e57b18d27b1
code eqn for slice was missing; redefined splice with fun
nipkow
parents:
40365
diff
changeset

222 
"splice (x#xs) (y#ys) = x # y # splice xs ys" 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

223 

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

226 
\fbox{ 

227 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

34978
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

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

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

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

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

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

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

267 
\label{fig:Characteristic} 

268 
\end{figure} 

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

272 

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

275 

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

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

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

278 

39915
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

279 
inductive sorted :: "'a list \<Rightarrow> bool" where 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

280 
Nil [iff]: "sorted []" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

281 
 Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

282 

ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

283 
lemma sorted_single [iff]: 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

284 
"sorted [x]" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

285 
by (rule sorted.Cons) auto 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

286 

ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

287 
lemma sorted_many: 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

288 
"x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

289 
by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto) 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

290 

ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

291 
lemma sorted_many_eq [simp, code]: 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

292 
"sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

293 
by (auto intro: sorted_many elim: sorted.cases) 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

294 

ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

295 
lemma [code]: 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

296 
"sorted [] \<longleftrightarrow> True" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

297 
"sorted [x] \<longleftrightarrow> True" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

298 
by simp_all 
24697  299 

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

300 
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

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

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

303 

35195  304 
definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
305 
"sort_key f xs = foldr (insort_key f) xs []" 

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

306 

40210
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

307 
definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

308 
"insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)" 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

309 

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

310 
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

311 
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)" 
40210
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

312 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  313 

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

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

315 

24616  316 

23388  317 
subsubsection {* List comprehension *} 
23192  318 

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

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

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

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

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

325 

326 
The qualifiers after the dot are 

327 
\begin{description} 

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

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

329 
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

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

331 
%\item[local bindings] @ {text"let x = e"}. 
24349  332 
\end{description} 
23240  333 

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

334 
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

335 
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

336 
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

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

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

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

342 
definitions for the list comprehensions in question. *} 

343 

42144
15218eb98fd7
list comprehension: strip positions where the translation cannot handle them right now;
wenzelm
parents:
42057
diff
changeset

344 
nonterminal lc_gen and lc_qual and lc_quals 
23192  345 

346 
syntax 

23240  347 
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __") 
42144
15218eb98fd7
list comprehension: strip positions where the translation cannot handle them right now;
wenzelm
parents:
42057
diff
changeset

348 
"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ < _") 
23240  349 
"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_") 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

350 
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*) 
23240  351 
"_lc_end" :: "lc_quals" ("]") 
352 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 

24349  353 
"_lc_abs" :: "'a => 'b list => 'b list" 
42144
15218eb98fd7
list comprehension: strip positions where the translation cannot handle them right now;
wenzelm
parents:
42057
diff
changeset

354 
"_strip_positions" :: "'a \<Rightarrow> lc_gen" ("_") 
23192  355 

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

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

357 
translation of [e. p<xs] 
23192  358 
translations 
24349  359 
"[e. p<xs]" => "concat(map (_lc_abs p [e]) xs)" 
23240  360 
"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" 
24349  361 
=> "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)" 
23240  362 
"[e. P]" => "if P then [e] else []" 
363 
"_listcompr e (_lc_test P) (_lc_quals Q Qs)" 

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

24349  365 
"_listcompr e (_lc_let b) (_lc_quals Q Qs)" 
366 
=> "_Let b (_listcompr e Q Qs)" 

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

367 
*) 
23240  368 

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

369 
syntax (xsymbols) 
42144
15218eb98fd7
list comprehension: strip positions where the translation cannot handle them right now;
wenzelm
parents:
42057
diff
changeset

370 
"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

371 
syntax (HTML output) 
42144
15218eb98fd7
list comprehension: strip positions where the translation cannot handle them right now;
wenzelm
parents:
42057
diff
changeset

372 
"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
24349  373 

374 
parse_translation (advanced) {* 

375 
let 

35256  376 
val NilC = Syntax.const @{const_syntax Nil}; 
377 
val ConsC = Syntax.const @{const_syntax Cons}; 

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

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

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

35115  381 

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

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

383 

35115  384 
fun pat_tr ctxt p e opti = (* %x. case x of p => e  _ => [] *) 
24349  385 
let 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
42871
diff
changeset

386 
(* FIXME proper name context!? *) 
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
42871
diff
changeset

387 
val x = Free (singleton (Name.variant_list (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

388 
val e = if opti then singl e else e; 
42264  389 
val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e; 
35256  390 
val case2 = 
391 
Syntax.const @{syntax_const "_case1"} $ 

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

35115  393 
val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; 
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors  side effect: function package correctly identifies 0::int as a nonconstructor;
krauss
parents:
43324
diff
changeset

394 
val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs]; 
24349  395 
in lambda x ft end; 
396 

35256  397 
fun abs_tr ctxt (p as Free (s, T)) e opti = 
35115  398 
let 
42361  399 
val thy = Proof_Context.theory_of ctxt; 
400 
val s' = Proof_Context.intern_const ctxt s; 

35115  401 
in 
402 
if Sign.declared_const thy s' 

403 
then (pat_tr ctxt p e opti, false) 

404 
else (lambda p e, true) 

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

406 
 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

407 

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

410 
val res = 

411 
(case qs of 

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

413 
 Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]); 

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

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

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

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

418 
(case abs_tr ctxt p e true of 
35115  419 
(f, true) => mapC $ f $ es 
420 
 (f, false) => concatC $ (mapC $ f $ es)) 

421 
 lc_tr ctxt 

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

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

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

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

426 

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

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

429 

42167  430 
ML {* 
431 
let 

432 
val read = Syntax.read_term @{context}; 

433 
fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1); 

434 
in 

435 
check "[(x,y,z). b]" "if b then [(x, y, z)] else []"; 

436 
check "[(x,y,z). x\<leftarrow>xs]" "map (\<lambda>x. (x, y, z)) xs"; 

437 
check "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]" "concat (map (\<lambda>x. map (\<lambda>y. e x y) ys) xs)"; 

438 
check "[(x,y,z). x<a, x>b]" "if x < a then if b < x then [(x, y, z)] else [] else []"; 

439 
check "[(x,y,z). x\<leftarrow>xs, x>b]" "concat (map (\<lambda>x. if b < x then [(x, y, z)] else []) xs)"; 

440 
check "[(x,y,z). x<a, x\<leftarrow>xs]" "if x < a then map (\<lambda>x. (x, y, z)) xs else []"; 

441 
check "[(x,y). Cons True x \<leftarrow> xs]" 

442 
"concat (map (\<lambda>xa. case xa of [] \<Rightarrow> []  True # x \<Rightarrow> [(x, y)]  False # x \<Rightarrow> []) xs)"; 

443 
check "[(x,y,z). Cons x [] \<leftarrow> xs]" 

444 
"concat (map (\<lambda>xa. case xa of [] \<Rightarrow> []  [x] \<Rightarrow> [(x, y, z)]  x # aa # lista \<Rightarrow> []) xs)"; 

445 
check "[(x,y,z). x<a, x>b, x=d]" 

446 
"if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []"; 

447 
check "[(x,y,z). x<a, x>b, y\<leftarrow>ys]" 

448 
"if x < a then if b < x then map (\<lambda>y. (x, y, z)) ys else [] else []"; 

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

450 
"if x < a then concat (map (\<lambda>x. if b < y then [(x, y, z)] else []) xs) else []"; 

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

452 
"if x < a then concat (map (\<lambda>x. map (\<lambda>y. (x, y, z)) ys) xs) else []"; 

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

454 
"concat (map (\<lambda>x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)"; 

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

456 
"concat (map (\<lambda>x. if b < x then map (\<lambda>y. (x, y, z)) ys else []) xs)"; 

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

458 
"concat (map (\<lambda>x. concat (map (\<lambda>y. if x < y then [(x, y, z)] else []) ys)) xs)"; 

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

460 
"concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)" 

461 
end; 

462 
*} 

463 

35115  464 
(* 
24349  465 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  466 
*) 
467 

42167  468 

41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

469 
use "Tools/list_to_set_comprehension.ML" 
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

470 

edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

471 
simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *} 
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

472 

35115  473 

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

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

475 

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

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

477 
"xs \<noteq> x # xs" 
13145  478 
by (induct xs) auto 
13114  479 

41697  480 
lemma not_Cons_self2 [simp]: 
481 
"x # xs \<noteq> xs" 

482 
by (rule not_Cons_self [symmetric]) 

13114  483 

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

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

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

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

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

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

495 
shows "P xs" 

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

497 
case Nil then show ?case by simp 

498 
next 

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

500 
case Nil with single show ?thesis by simp 

501 
next 

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

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

504 
ultimately show ?thesis by (rule cons) 

505 
qed 

506 
qed 

507 

13114  508 

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

509 
subsubsection {* @{const length} *} 
13114  510 

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

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

513 
append_eq_append_conv}. 
13142  514 
*} 
13114  515 

13142  516 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  517 
by (induct xs) auto 
13114  518 

13142  519 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  520 
by (induct xs) auto 
13114  521 

13142  522 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  523 
by (induct xs) auto 
13114  524 

13142  525 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  526 
by (cases xs) auto 
13114  527 

13142  528 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  529 
by (induct xs) auto 
13114  530 

13142  531 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  532 
by (induct xs) auto 
13114  533 

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

536 

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

13142  540 

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

14208  543 
apply (induct xs, simp, simp) 
14025  544 
apply blast 
545 
done 

546 

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

547 
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

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

549 

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

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

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

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

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

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

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

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

557 
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

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

559 

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

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

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

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

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

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

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

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

567 
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

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

569 
qed 
13114  570 

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

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

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

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

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

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

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

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

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

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

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

581 

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

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

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

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

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

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

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

588 
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

589 

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

590 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  591 
by (rule Eq_FalseI) auto 
24037  592 

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

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

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

595 
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

596 
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

597 
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

598 
*) 
24037  599 

600 
let 

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

601 

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

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

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

606 
 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

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

608 

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

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

612 
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

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

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

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

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

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

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

622 
in 
23214  623 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
624 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

629 

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

630 

15392  631 
subsubsection {* @{text "@"}  append *} 
13114  632 

13142  633 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  634 
by (induct xs) auto 
13114  635 

13142  636 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  637 
by (induct xs) auto 
3507  638 

13142  639 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  640 
by (induct xs) auto 
13114  641 

13142  642 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  643 
by (induct xs) auto 
13114  644 

13142  645 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  646 
by (induct xs) auto 
13114  647 

13142  648 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  649 
by (induct xs) auto 
13114  650 

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

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

653 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  654 
apply (induct xs arbitrary: ys) 
14208  655 
apply (case_tac ys, simp, force) 
656 
apply (case_tac ys, force, simp) 

13145  657 
done 
13142  658 

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

661 
apply (induct xs arbitrary: ys zs ts) 

14495  662 
apply fastsimp 
663 
apply(case_tac zs) 

664 
apply simp 

665 
apply fastsimp 

666 
done 

667 

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

668 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  669 
by simp 
13142  670 

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

13145  672 
by simp 
13114  673 

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

674 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  675 
by simp 
13114  676 

13142  677 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  678 
using append_same_eq [of _ _ "[]"] by auto 
3507  679 

13142  680 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  681 
using append_same_eq [of "[]"] by auto 
13114  682 

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

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

13142  686 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  687 
by (induct xs) auto 
13114  688 

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

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

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

698 

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

701 
by(cases ys) auto 

702 

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

705 
by(cases ys) auto 

706 

14300  707 

13142  708 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  709 

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

13145  711 
by simp 
13114  712 

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

13114  716 

13142  717 
lemma append_eq_appendI: 
13145  718 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
719 
by (drule sym) simp 

13114  720 

721 

13142  722 
text {* 
13145  723 
Simplification procedure for all list equalities. 
724 
Currently only tries to rearrange @{text "@"} to see if 

725 
 both lists end in a singleton list, 

726 
 or both lists end in the same list. 

13142  727 
*} 
728 

43594  729 
simproc_setup list_eq ("(xs::'a list) = ys") = {* 
13462  730 
let 
43594  731 
fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) = 
732 
(case xs of Const (@{const_name Nil}, _) => cons  _ => last xs) 

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

734 
 last t = t; 

735 

736 
fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true 

737 
 list1 _ = false; 

738 

739 
fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) = 

740 
(case xs of Const (@{const_name Nil}, _) => xs  _ => cons $ butlast xs) 

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

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

743 

744 
val rearr_ss = 

745 
HOL_basic_ss addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]; 

746 

747 
fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 

13462  748 
let 
43594  749 
val lastl = last lhs and lastr = last rhs; 
750 
fun rearr conv = 

751 
let 

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

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

754 
val appT = [listT,listT] > listT 

755 
val app = Const(@{const_name append},appT) 

756 
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr) 

757 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2)); 

758 
val thm = Goal.prove (Simplifier.the_context ss) [] [] eq 

759 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 

760 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 

761 
in 

762 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 

763 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

764 
else NONE 

765 
end; 

766 
in fn _ => fn ss => fn ct => list_eq ss (term_of ct) end; 

13114  767 
*} 
768 

769 

15392  770 
subsubsection {* @{text map} *} 
13114  771 

40210
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

772 
lemma hd_map: 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

773 
"xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)" 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

774 
by (cases xs) simp_all 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

775 

aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

776 
lemma map_tl: 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

777 
"map f (tl xs) = tl (map f xs)" 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

778 
by (cases xs) simp_all 
aee7ef725330
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
haftmann
parents:
40195
diff
changeset

779 

13142  780 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  781 
by (induct xs) simp_all 
13114  782 

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

13142  786 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  787 
by (induct xs) auto 
13114  788 

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

789 
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

790 
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

791 

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

794 
apply(simp) 

795 
done 

796 

13142  797 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  798 
by (induct xs) auto 
13114  799 

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

802 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
43594
diff
changeset

803 
lemma map_cong [fundef_cong]: 
40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

804 
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys" 
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

805 
by simp 
13114  806 

13142  807 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  808 
by (cases xs) auto 
13114  809 

13142  810 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  811 
by (cases xs) auto 
13114  812 

18447  813 
lemma map_eq_Cons_conv: 
14025  814 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  815 
by (cases xs) auto 
13114  816 

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

820 

18447  821 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
822 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

823 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

824 

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

18447  827 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  828 

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

829 
lemma map_eq_imp_length_eq: 
35510  830 
assumes "map f xs = map g ys" 
26734  831 
shows "length xs = length ys" 
832 
using assms proof (induct ys arbitrary: xs) 

833 
case Nil then show ?case by simp 

834 
next 

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

35510  836 
from Cons xs have "map f zs = map g ys" by simp 
26734  837 
moreover with Cons have "length zs = length ys" by blast 
838 
with xs show ?case by simp 

839 
qed 

840 

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

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

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

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

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

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

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

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

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

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

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

851 

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

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

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

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

855 

13114  856 
lemma map_injective: 
24526  857 
"map f xs = map f ys ==> inj f ==> xs = ys" 
858 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  859 

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

862 

13114  863 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  864 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  865 

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

14208  867 
apply (unfold inj_on_def, clarify) 
13145  868 
apply (erule_tac x = "[x]" in ballE) 
14208  869 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  870 
apply blast 
871 
done 

13114  872 

14339  873 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  874 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  875 

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

878 
apply(erule map_inj_on) 

879 
apply(blast intro:inj_onI dest:inj_onD) 

880 
done 

881 

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

13114  884 

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

885 
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

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

887 

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

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

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

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

891 

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

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

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

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

895 

41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41463
diff
changeset

896 
enriched_type map: map 
41372  897 
by (simp_all add: fun_eq_iff id_def) 
40608
6c28ab8b8166
mapper for list type; map_pair replaces prod_fun
haftmann
parents:
40593
diff
changeset

898 

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

899 

15392  900 
subsubsection {* @{text rev} *} 
13114  901 

13142  902 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  903 
by (induct xs) auto 
13114  904 

13142  905 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  906 
by (induct xs) auto 
13114  907 

15870  908 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
909 
by auto 

910 

13142  911 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  912 
by (induct xs) auto 
13114  913 

13142  914 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  915 
by (induct xs) auto 
13114  916 

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

919 

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

921 
by (cases xs) auto 

922 

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

923 
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

924 
apply (induct xs arbitrary: ys, force) 
14208  925 
apply (case_tac ys, simp, force) 
13145  926 
done 
13114  927 

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

930 

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

933 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  934 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
935 
done 

13114  936 

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

13145  939 
by (induct xs rule: rev_induct) auto 
13114  940 

13366  941 
lemmas rev_cases = rev_exhaust 
942 

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

945 

13114  946 

15392  947 
subsubsection {* @{text set} *} 
13114  948 

13142  949 
lemma finite_set [iff]: "finite (set xs)" 
13145  950 
by (induct xs) auto 
13114  951 

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

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

14099  957 

13142  958 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  959 
by auto 
13114  960 

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

963 

13142  964 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  965 
by (induct xs) auto 
13114  966 

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

969 

13142  970 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  971 
by (induct xs) auto 
13114  972 

13142  973 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  974 
by (induct xs) auto 
13114  975 

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

32417  979 
lemma set_upt [simp]: "set[i..<j] = {i..<j}" 
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

980 
by (induct j) auto 
13114  981 

13142  982 

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

983 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  984 
proof (induct xs) 
26073  985 
case Nil thus ?case by simp 
986 
next 

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

988 
qed 

989 

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

26073  992 

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

994 
proof (induct xs) 

995 
case Nil thus ?case by simp 

18049  996 
next 
997 
case (Cons a xs) 

998 
show ?case 

999 
proof cases 

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

1000 
assume "x = a" thus ?case using Cons by fastsimp 
18049  1001 
next 
26073  1002 
assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI) 
1003 
qed 

1004 
qed 

1005 

1006 
lemma in_set_conv_decomp_first: 

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

26734  1008 
by (auto dest!: split_list_first) 
26073  1009 

40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

1010 
lemma split_list_last: "x \<in> set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs" 
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

1011 
proof (induct xs rule: rev_induct) 
26073  1012 
case Nil thus ?case by simp 
1013 
next 

1014 
case (snoc a xs) 

1015 
show ?case 

1016 
proof cases 

40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

1017 
assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE) 
26073  1018 
next 
1019 
assume "x \<noteq> a" thus ?case using snoc by fastsimp 

18049  1020 
qed 
1021 
qed 

1022 

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

26734  1025 
by (auto dest!: split_list_last) 
26073  1026 

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

1028 
proof (induct xs) 

1029 
case Nil thus ?case by simp 

1030 
next 

1031 
case Cons thus ?case 

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

1033 
qed 

1034 

1035 
lemma split_list_propE: 

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

1038 
using split_list_prop [OF assms] by blast 

26073  1039 

1040 
lemma split_list_first_prop: 

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

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

26734  1043 
proof (induct xs) 
26073  1044 
case Nil thus ?case by simp 
1045 
next 

1046 
case (Cons x xs) 

1047 
show ?case 

1048 
proof cases 

1049 
assume "P x" 

40122
1d8ad2ff3e01
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
haftmann
parents:
40077
diff
changeset

1050 
thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 
26073  1051 
next 
1052 
assume "\<not> P x" 

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

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

1055 
qed 

1056 
qed 

1057 

1058 
lemma split_list_first_propE: 

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

1061 
using split_list_first_prop [OF assms] by blast 

26073  1062 

1063 
lemma split_list_first_prop_iff: 

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

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

26734  1066 
by (rule, erule split_list_first_prop) auto 
26073  1067 

1068 
lemma split_list_last_prop: 

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

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

1071 
proof(induct xs rule:rev_induct) 

1072 
case Nil thus ?case by simp 

1073 
next 

1074 
case (snoc x xs) 

1075 
show ?case 

1076 
proof cases 

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

1078 
next 

1079 
assume "\<not> P x" 

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

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

1082 
qed 

1083 
qed 

1084 

1085 
lemma split_list_last_propE: 

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

1088 
using split_list_last_prop [OF assms] by blast 

26073  1089 

1090 
lemma split_list_last_prop_iff: 

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

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

26734  1093 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1094 

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

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

13508  1098 

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

13114  1101 

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

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

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

1104 
by (induct xs) auto 
15168  1105 

35115  1106 

15392  1107 
subsubsection {* @{text filter} *} 
13114  1108 

13142  1109 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1110 
by (induct xs) auto 
13114  1111 

15305  1112 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1113 
by (induct xs) simp_all 

1114 

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

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

1120 

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

1123 
by(induct xs) simp_all 

1124 

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

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

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

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

1135 
apply (induct xs) 

1136 
apply auto 

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

1138 
apply simp 

1139 
done 

13114  1140 

16965  1141 
lemma filter_map: 
1142 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1143 
by (induct xs) simp_all 

1144 

1145 
lemma length_filter_map[simp]: 

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

1147 
by (simp add:filter_map) 

1148 

13142  1149 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1150 
by auto 
13114  1151 

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

1154 
proof (induct xs) 

1155 
case Nil thus ?case by simp 

1156 
next 

1157 
case (Cons x xs) thus ?case 

1158 
apply (auto split:split_if_asm) 

1159 
using length_filter_le[of P xs] apply arith 

1160 
done 

1161 
qed 

13114  1162 

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

1165 
proof (induct xs) 

1166 
case Nil thus ?case by simp 

1167 
next 

1168 
case (Cons x xs) 

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

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

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

1172 
proof (cases) 

1173 
assume "p x" 

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

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

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

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

1182 
finally show ?thesis . 

1183 
next 

1184 
assume "\<not> p x" 

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

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

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

1192 
by (simp add:card_insert_if) 

1193 
finally show ?thesis . 

1194 
qed 

1195 
qed 

1196 

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

1199 
\<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  1200 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1201 
proof(induct ys) 
1202 
case Nil thus ?case by simp 

1203 
next 

1204 
case (Cons y ys) 

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

1206 
proof cases 

1207 
assume Py: "P y" 

1208 
show ?thesis 

1209 
proof cases 

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

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

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

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

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

1215 
with Py Cons.prems show ?thesis by simp 
17629  1216 
qed 
1217 
next 

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

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

1219 
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

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

1221 
then show ?thesis .. 
17629  1222 
qed 
1223 
qed 

1224 

1225 
lemma filter_eq_ConsD: 

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

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

1228 
by(rule Cons_eq_filterD) simp 

1229 

1230 
lemma filter_eq_Cons_iff: 

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

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

1233 
by(auto dest:filter_eq_ConsD) 

1234 

1235 
lemma Cons_eq_filter_iff: 

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

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

1238 
by(auto dest:Cons_eq_filterD) 

1239 

44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
43594
diff
changeset

1240 
lemma filter_cong[fundef_cong]: 
17501  1241 
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys" 
1242 
apply simp 

1243 
apply(erule thin_rl) 

1244 
by (induct ys) simp_all 

1245 

15281  1246 

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

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

1248 

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

1249 
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

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

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

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

1253 
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

1254 

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

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

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

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

1258 

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

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

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

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

1262 

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

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

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

1265 
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

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

1267 
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

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

1269 
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

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

1271 

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

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

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

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

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

1276 
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

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

1278 
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

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

1280 

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

1281 
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

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

1283 
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

1284 
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

1285 

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

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

1287 

35115  1288 

15392  1289 
subsubsection {* @{text concat} *} 
13114  1290 

13142  1291 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1292 
by (induct xs) auto 
13114  1293 

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

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

24308  1300 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1301 
by (induct xs) auto 
13114  1302 

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

1303 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1304 
by (induct xs) auto 
1305 

13142  1306 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1307 
by (induct xs) auto 
13114  1308 

13142  1309 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1310 
by (induct xs) auto 
13114  1311 

13142  1312 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1313 
by (induct xs) auto 
13114  1314 

40365
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1315 
lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)" 
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1316 
proof (induct xs arbitrary: ys) 
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1317 
case (Cons x xs ys) 
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1318 
thus ?case by (cases ys) auto 
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1319 
qed (auto) 
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1320 

a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1321 
lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \<forall>(x, y) \<in> set (zip xs ys). length x = length y ==> xs = ys" 
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1322 
by (simp add: concat_eq_concat_iff) 
a1456f2e1c9d
added two lemmas about injectivity of concat to the list theory
bulwahn
parents:
40304
diff
changeset

1323 

13114  1324 

15392  1325 
subsubsection {* @{text nth} *} 
13114  1326 

29827  1327 
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" 
13145  1328 
by auto 
13114  1329 

29827  1330 
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n" 
13145 