author  berghofe 
Tue, 10 Jan 2012 18:12:03 +0100  
changeset 46176  1898e61e89c4 
parent 46156  f58b7f9d3920 
child 46313  0c4f18fe8218 
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 

46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

52 
definition 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

53 
coset :: "'a list \<Rightarrow> 'a set" where 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

54 
[simp]: "coset xs =  set xs" 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

55 

34941  56 
primrec 
57 
map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where 

58 
"map f [] = []" 

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

60 

61 
primrec 

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

63 
append_Nil:"[] @ ys = ys" 

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

65 

66 
primrec 

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

68 
"rev [] = []" 

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

70 

71 
primrec 

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

73 
"filter P [] = []" 

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

75 

76 
syntax 

77 
 {* Special syntax for filter *} 

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

80 
translations 

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

82 

83 
syntax (xsymbols) 

35115  84 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  85 
syntax (HTML output) 
35115  86 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  87 

46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

88 
primrec  {* canonical argument order *} 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

89 
fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

90 
"fold f [] = id" 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

91 
 "fold f (x # xs) = fold f xs \<circ> f x" 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

92 

d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

93 
definition 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

94 
foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

95 
[code_abbrev]: "foldr f xs = fold f (rev xs)" 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

96 

d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

97 
definition 
34941  98 
foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where 
46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

99 
"foldl f s xs = fold (\<lambda>x s. f s x) xs s" 
34941  100 

101 
primrec 

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

103 
"concat [] = []" 

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

105 

39774  106 
definition (in monoid_add) 
34941  107 
listsum :: "'a list \<Rightarrow> 'a" where 
39774  108 
"listsum xs = foldr plus xs 0" 
34941  109 

110 
primrec 

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

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

113 
 drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs  Suc m \<Rightarrow> drop 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 
take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

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

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

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

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

123 

124 
primrec 

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

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

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

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

129 

130 
primrec 

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

132 
"list_update [] i v = []" 

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

923  134 

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

135 
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

136 

923  137 
syntax 
13366  138 
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") 
139 
"" :: "lupdbind => lupdbinds" ("_") 

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

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

142 

923  143 
translations 
35115  144 
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" 
34941  145 
"xs[i:=x]" == "CONST list_update xs i x" 
146 

147 
primrec 

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

149 
"takeWhile P [] = []" 

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

151 

152 
primrec 

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

154 
"dropWhile P [] = []" 

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

156 

157 
primrec 

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

159 
"zip xs [] = []" 

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

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

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

163 

164 
primrec 

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

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

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

168 

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

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

170 
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

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

172 

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

173 
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

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

175 

34941  176 
primrec 
177 
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

178 
"remove1 x [] = []" 

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

180 

181 
primrec 

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

183 
"removeAll x [] = []" 

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

185 

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

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

187 
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

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

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

190 

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

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

192 
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

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

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

195 

34941  196 
primrec 
197 
replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 

198 
replicate_0: "replicate 0 x = []" 

199 
 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

200 

13142  201 
text {* 
14589  202 
Function @{text size} is overloaded for all datatypes. Users may 
13366  203 
refer to the list version as @{text length}. *} 
13142  204 

19363  205 
abbreviation 
34941  206 
length :: "'a list \<Rightarrow> nat" where 
207 
"length \<equiv> size" 

15307  208 

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

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

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

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

212 

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

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

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

216 

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

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

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

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

221 

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

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

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

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

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

226 
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

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

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

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

230 

26771  231 
text{* 
232 
\begin{figure}[htbp] 

233 
\fbox{ 

234 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

246 
@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\ 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

247 
@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\ 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

248 
@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\ 
27381  249 
@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\ 
250 
@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ 

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

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

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

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

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

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

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

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

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

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

261 
@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ 
35295  262 
@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\ 
27381  263 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  264 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  265 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
266 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

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

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

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

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

46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

272 
@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)} 
26771  273 
\end{tabular}} 
274 
\caption{Characteristic examples} 

275 
\label{fig:Characteristic} 

276 
\end{figure} 

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

280 

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

283 

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

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

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

286 

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

287 
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

288 
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

289 
 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

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_single [iff]: 
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]" 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

293 
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

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 sorted_many: 
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

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

297 
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

298 

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

299 
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

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

301 
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

302 

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

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

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

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

306 
by simp_all 
24697  307 

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

308 
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

309 
"insort_key f x [] = [x]"  
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

310 
"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))" 
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

311 

35195  312 
definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

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

314 

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

315 
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

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

317 

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

318 
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

319 
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

320 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  321 

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

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

323 

24616  324 

23388  325 
subsubsection {* List comprehension *} 
23192  326 

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

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

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

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

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

333 

334 
The qualifiers after the dot are 

335 
\begin{description} 

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

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

337 
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

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

339 
%\item[local bindings] @ {text"let x = e"}. 
24349  340 
\end{description} 
23240  341 

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

342 
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

343 
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

344 
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

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

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

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

350 
definitions for the list comprehensions in question. *} 

351 

46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

352 
nonterminal lc_qual and lc_quals 
23192  353 

354 
syntax 

46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

355 
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __") 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

356 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ < _") 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

357 
"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_") 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

358 
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*) 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

359 
"_lc_end" :: "lc_quals" ("]") 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

360 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

361 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  362 

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

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

364 
translation of [e. p<xs] 
23192  365 
translations 
46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

366 
"[e. p<xs]" => "concat(map (_lc_abs p [e]) xs)" 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

367 
"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

368 
=> "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)" 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

369 
"[e. P]" => "if P then [e] else []" 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

370 
"_listcompr e (_lc_test P) (_lc_quals Q Qs)" 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

371 
=> "if P then (_listcompr e Q Qs) else []" 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

372 
"_listcompr e (_lc_let b) (_lc_quals Q Qs)" 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

373 
=> "_Let b (_listcompr e Q Qs)" 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

374 
*) 
23240  375 

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

376 
syntax (xsymbols) 
46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

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

378 
syntax (HTML output) 
46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

379 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
24349  380 

381 
parse_translation (advanced) {* 

46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

382 
let 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

383 
val NilC = Syntax.const @{const_syntax Nil}; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

384 
val ConsC = Syntax.const @{const_syntax Cons}; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

385 
val mapC = Syntax.const @{const_syntax map}; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

386 
val concatC = Syntax.const @{const_syntax concat}; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

387 
val IfC = Syntax.const @{const_syntax If}; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

388 

85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

389 
fun single x = ConsC $ x $ NilC; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

390 

85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

391 
fun pat_tr ctxt p e opti = (* %x. case x of p => e  _ => [] *) 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

392 
let 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

393 
(* FIXME proper name context!? *) 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

394 
val x = 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

395 
Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT); 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

396 
val e = if opti then single e else e; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

397 
val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

398 
val case2 = 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

399 
Syntax.const @{syntax_const "_case1"} $ 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

400 
Syntax.const @{const_syntax dummy_pattern} $ NilC; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

401 
val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

402 
in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr false ctxt [x, cs]] end; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

403 

85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

404 
fun abs_tr ctxt p e opti = 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

405 
(case Term_Position.strip_positions p of 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

406 
Free (s, T) => 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

407 
let 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

408 
val thy = Proof_Context.theory_of ctxt; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

409 
val s' = Proof_Context.intern_const ctxt s; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

410 
in 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

411 
if Sign.declared_const thy s' 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

412 
then (pat_tr ctxt p e opti, false) 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

413 
else (Syntax_Trans.abs_tr [p, e], true) 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

414 
end 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

415 
 _ => (pat_tr ctxt p e opti, false)); 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

416 

85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

417 
fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] = 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

418 
let 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

419 
val res = 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

420 
(case qs of 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

421 
Const (@{syntax_const "_lc_end"}, _) => single e 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

422 
 Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]); 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

423 
in IfC $ b $ res $ NilC end 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

424 
 lc_tr ctxt 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

425 
[e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

426 
Const(@{syntax_const "_lc_end"}, _)] = 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

427 
(case abs_tr ctxt p e true of 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

428 
(f, true) => mapC $ f $ es 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

429 
 (f, false) => concatC $ (mapC $ f $ es)) 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

430 
 lc_tr ctxt 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

431 
[e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es, 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

432 
Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] = 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

433 
let val e' = lc_tr ctxt [e, q, qs]; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

434 
in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end; 
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

435 

85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

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

438 

42167  439 
ML {* 
440 
let 

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

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

443 
in 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

470 
end; 

471 
*} 

472 

35115  473 
(* 
24349  474 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  475 
*) 
476 

42167  477 

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

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

479 

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

480 
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

481 

46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

482 
code_datatype set coset 
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

483 

d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
46125
diff
changeset

484 
hide_const (open) coset 
35115  485 

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

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

487 

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

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

489 
"xs \<noteq> x # xs" 
13145  490 
by (induct xs) auto 
13114  491 

41697  492 
lemma not_Cons_self2 [simp]: 
493 
"x # xs \<noteq> xs" 

494 
by (rule not_Cons_self [symmetric]) 

13114  495 

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

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

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

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

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

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

507 
shows "P xs" 

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

509 
case Nil then show ?case by simp 

510 
next 

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

512 
case Nil with single show ?thesis by simp 

513 
next 

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

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

516 
ultimately show ?thesis by (rule cons) 

517 
qed 

518 
qed 

519 

45714  520 
lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X" 
521 
by (auto intro!: inj_onI) 

13114  522 

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

523 
subsubsection {* @{const length} *} 
13114  524 

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

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

527 
append_eq_append_conv}. 
13142  528 
*} 
13114  529 

13142  530 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  531 
by (induct xs) auto 
13114  532 

13142  533 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  534 
by (induct xs) auto 
13114  535 

13142  536 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  537 
by (induct xs) auto 
13114  538 

13142  539 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  540 
by (cases xs) auto 
13114  541 

13142  542 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  543 
by (induct xs) auto 
13114  544 

13142  545 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  546 
by (induct xs) auto 
13114  547 

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

550 

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

13142  554 

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

14208  557 
apply (induct xs, simp, simp) 
14025  558 
apply blast 
559 
done 

560 

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

561 
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

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

563 

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

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

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

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

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

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

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

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

571 
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

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

573 

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

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

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

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

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

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

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

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

581 
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

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

583 
qed 
13114  584 

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

585 
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

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

587 
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

588 
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

589 
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

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

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

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

593 
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

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

595 

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

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

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

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

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

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

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

602 
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

603 

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

604 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  605 
by (rule Eq_FalseI) auto 
24037  606 

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

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

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

609 
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

610 
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

611 
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

612 
*) 
24037  613 

614 
let 

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

615 

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

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

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

620 
 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

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

622 

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

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

626 
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

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

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

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

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

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

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

636 
in 
23214  637 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
638 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

643 

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

644 

15392  645 
subsubsection {* @{text "@"}  append *} 
13114  646 

13142  647 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  648 
by (induct xs) auto 
13114  649 

13142  650 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  651 
by (induct xs) auto 
3507  652 

13142  653 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  654 
by (induct xs) auto 
13114  655 

13142  656 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  657 
by (induct xs) auto 
13114  658 

13142  659 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  660 
by (induct xs) auto 
13114  661 

13142  662 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  663 
by (induct xs) auto 
13114  664 

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

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

667 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  668 
apply (induct xs arbitrary: ys) 
14208  669 
apply (case_tac ys, simp, force) 
670 
apply (case_tac ys, force, simp) 

13145  671 
done 
13142  672 

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

675 
apply (induct xs arbitrary: ys zs ts) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

676 
apply fastforce 
14495  677 
apply(case_tac zs) 
678 
apply simp 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

679 
apply fastforce 
14495  680 
done 
681 

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

682 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  683 
by simp 
13142  684 

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

13145  686 
by simp 
13114  687 

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

688 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  689 
by simp 
13114  690 

13142  691 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  692 
using append_same_eq [of _ _ "[]"] by auto 
3507  693 

13142  694 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  695 
using append_same_eq [of "[]"] by auto 
13114  696 

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

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

13142  700 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  701 
by (induct xs) auto 
13114  702 

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

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

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

712 

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

715 
by(cases ys) auto 

716 

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

719 
by(cases ys) auto 

720 

14300  721 

13142  722 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  723 

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

13145  725 
by simp 
13114  726 

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

13114  730 

13142  731 
lemma append_eq_appendI: 
13145  732 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
733 
by (drule sym) simp 

13114  734 

735 

13142  736 
text {* 
13145  737 
Simplification procedure for all list equalities. 
738 
Currently only tries to rearrange @{text "@"} to see if 

739 
 both lists end in a singleton list, 

740 
 or both lists end in the same list. 

13142  741 
*} 
742 

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

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

748 
 last t = t; 

749 

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

751 
 list1 _ = false; 

752 

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

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

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

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

757 

758 
val rearr_ss = 

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

760 

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

13462  762 
let 
43594  763 
val lastl = last lhs and lastr = last rhs; 
764 
fun rearr conv = 

765 
let 

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

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

768 
val appT = [listT,listT] > listT 

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

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

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

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

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

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

775 
in 

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

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

778 
else NONE 

779 
end; 

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

13114  781 
*} 
782 

783 

15392  784 
subsubsection {* @{text map} *} 
13114  785 

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

786 
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

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

788 
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

789 

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

790 
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

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

792 
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

793 

13142  794 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  795 
by (induct xs) simp_all 
13114  796 

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

13142  800 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  801 
by (induct xs) auto 
13114  802 

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

803 
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

804 
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

805 

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

808 
apply(simp) 

809 
done 

810 

13142  811 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  812 
by (induct xs) auto 
13114  813 

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

816 

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

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

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

819 
by simp 
13114  820 

13142  821 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  822 
by (cases xs) auto 
13114  823 

13142  824 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  825 
by (cases xs) auto 
13114  826 

18447  827 
lemma map_eq_Cons_conv: 
14025  828 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  829 
by (cases xs) auto 
13114  830 

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

834 

18447  835 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
836 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

837 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

838 

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

18447  841 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  842 

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

843 
lemma map_eq_imp_length_eq: 
35510  844 
assumes "map f xs = map g ys" 
26734  845 
shows "length xs = length ys" 
846 
using assms proof (induct ys arbitrary: xs) 

847 
case Nil then show ?case by simp 

848 
next 

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

35510  850 
from Cons xs have "map f zs = map g ys" by simp 
26734  851 
moreover with Cons have "length zs = length ys" by blast 
852 
with xs show ?case by simp 

853 
qed 

854 

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

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

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

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

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

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

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

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

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

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

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

865 

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

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

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

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

869 

13114  870 
lemma map_injective: 
24526  871 
"map f xs = map f ys ==> inj f ==> xs = ys" 
872 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  873 

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

876 

13114  877 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  878 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  879 

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

14208  881 
apply (unfold inj_on_def, clarify) 
13145  882 
apply (erule_tac x = "[x]" in ballE) 
14208  883 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  884 
apply blast 
885 
done 

13114  886 

14339  887 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  888 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  889 

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

892 
apply(erule map_inj_on) 

893 
apply(blast intro:inj_onI dest:inj_onD) 

894 
done 

895 

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

13114  898 

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

899 
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

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

901 

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

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

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

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

905 

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

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

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

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

909 

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

910 
enriched_type map: map 
41372  911 
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

912 

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

913 

15392  914 
subsubsection {* @{text rev} *} 
13114  915 

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

13142  919 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  920 
by (induct xs) auto 
13114  921 

15870  922 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
923 
by auto 

924 

13142  925 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  926 
by (induct xs) auto 
13114  927 

13142  928 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  929 
by (induct xs) auto 
13114  930 

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

933 

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

935 
by (cases xs) auto 

936 

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

937 
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

938 
apply (induct xs arbitrary: ys, force) 
14208  939 
apply (case_tac ys, simp, force) 
13145  940 
done 
13114  941 

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

944 

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

947 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  948 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
949 
done 

13114  950 

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

13145  953 
by (induct xs rule: rev_induct) auto 
13114  954 

13366  955 
lemmas rev_cases = rev_exhaust 
956 

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

959 

13114  960 

15392  961 
subsubsection {* @{text set} *} 
13114  962 

13142  963 
lemma finite_set [iff]: "finite (set xs)" 
13145  964 
by (induct xs) auto 
13114  965 

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

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

14099  971 

13142  972 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  973 
by auto 
13114  974 

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

977 

13142  978 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  979 
by (induct xs) auto 
13114  980 

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

983 

13142  984 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  985 
by (induct xs) auto 
13114  986 

13142  987 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  988 
by (induct xs) auto 
13114  989 

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

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

994 
by (induct j) auto 
13114  995 

13142  996 

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

997 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  998 
proof (induct xs) 
26073  999 
case Nil thus ?case by simp 
1000 
next 

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

1002 
qed 

1003 

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

26073  1006 

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

1008 
proof (induct xs) 

1009 
case Nil thus ?case by simp 

18049  1010 
next 
1011 
case (Cons a xs) 

1012 
show ?case 

1013 
proof cases 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

1014 
assume "x = a" thus ?case using Cons by fastforce 
18049  1015 
next 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

1016 
assume "x \<noteq> a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI) 
26073  1017 
qed 
1018 
qed 

1019 

1020 
lemma in_set_conv_decomp_first: 

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

26734  1022 
by (auto dest!: split_list_first) 
26073  1023 

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

1024 
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

1025 
proof (induct xs rule: rev_induct) 
26073  1026 
case Nil thus ?case by simp 
1027 
next 

1028 
case (snoc a xs) 

1029 
show ?case 

1030 
proof cases 

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

1031 
assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE) 
26073  1032 
next 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

1033 
assume "x \<noteq> a" thus ?case using snoc by fastforce 
18049  1034 
qed 
1035 
qed 

1036 

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

26734  1039 
by (auto dest!: split_list_last) 
26073  1040 

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

1042 
proof (induct xs) 

1043 
case Nil thus ?case by simp 

1044 
next 

1045 
case Cons thus ?case 

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

1047 
qed 

1048 

1049 
lemma split_list_propE: 

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

1052 
using split_list_prop [OF assms] by blast 

26073  1053 

1054 
lemma split_list_first_prop: 

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

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

26734  1057 
proof (induct xs) 
26073  1058 
case Nil thus ?case by simp 
1059 
next 

1060 
case (Cons x xs) 

1061 
show ?case 

1062 
proof cases 

1063 
assume "P x" 

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

1064 
thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 
26073  1065 
next 
1066 
assume "\<not> P x" 

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

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

1069 
qed 

1070 
qed 

1071 

1072 
lemma split_list_first_propE: 

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

1075 
using split_list_first_prop [OF assms] by blast 

26073  1076 

1077 
lemma split_list_first_prop_iff: 

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

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

26734  1080 
by (rule, erule split_list_first_prop) auto 
26073  1081 

1082 
lemma split_list_last_prop: 

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

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

1085 
proof(induct xs rule:rev_induct) 

1086 
case Nil thus ?case by simp 

1087 
next 

1088 
case (snoc x xs) 

1089 
show ?case 

1090 
proof cases 

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

1092 
next 

1093 
assume "\<not> P x" 

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

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

1095 
thus ?thesis using `\<not> P x` snoc(1) by fastforce 
26073  1096 
qed 
1097 
qed 

1098 

1099 
lemma split_list_last_propE: 

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

1102 
using split_list_last_prop [OF assms] by blast 

26073  1103 

1104 
lemma split_list_last_prop_iff: 

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

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

26734  1107 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1108 

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

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

13508  1112 

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

13114  1115 

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

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

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

1118 
by (induct xs) auto 
15168  1119 

35115  1120 

15392  1121 
subsubsection {* @{text filter} *} 
13114  1122 

13142  1123 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1124 
by (induct xs) auto 
13114  1125 

15305  1126 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1127 
by (induct xs) simp_all 

1128 

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

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

1134 

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

1137 
by(induct xs) simp_all 

1138 

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

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

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

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

1149 
apply (induct xs) 

1150 
apply auto 

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

1152 
apply simp 

1153 
done 

13114  1154 

16965  1155 
lemma filter_map: 
1156 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1157 
by (induct xs) simp_all 

1158 

1159 
lemma length_filter_map[simp]: 

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

1161 
by (simp add:filter_map) 

1162 

13142  1163 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1164 
by auto 
13114  1165 

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

1168 
proof (induct xs) 

1169 
case Nil thus ?case by simp 

1170 
next 

1171 
case (Cons x xs) thus ?case 

1172 
apply (auto split:split_if_asm) 

1173 
using length_filter_le[of P xs] apply arith 

1174 
done 

1175 
qed 

13114  1176 

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

1179 
proof (induct xs) 

1180 
case Nil thus ?case by simp 

1181 
next 

1182 
case (Cons x xs) 

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

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

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

1186 
proof (cases) 

1187 
assume "p x" 

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

25162  1189 
by(auto simp: image_def split:nat.split dest:gr0_implies_Suc) 
15281  1190 
have "length (filter p (x # xs)) = Suc(card ?S)" 
23388  1191 
using Cons `p x` by simp 
15281  1192 
also have "\<dots> = Suc(card(Suc ` ?S))" using fin 
44921  1193 
by (simp add: card_image) 
15281  1194 
also have "\<dots> = card ?S'" using eq fin 
1195 
by (simp add:card_insert_if) (simp add:image_def) 

1196 
finally show ?thesis . 

1197 
next 

1198 
assume "\<not> p x" 

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

25162  1200 
by(auto simp add: image_def split:nat.split elim:lessE) 
15281  1201 
have "length (filter p (x # xs)) = card ?S" 
23388  1202 
using Cons `\<not> p x` by simp 
15281  1203 
also have "\<dots> = card(Suc ` ?S)" using fin 
44921  1204 
by (simp add: card_image) 
15281  1205 
also have "\<dots> = card ?S'" using eq fin 
1206 
by (simp add:card_insert_if) 

1207 
finally show ?thesis . 

1208 
qed 

1209 
qed 

1210 

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

1213 
\<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  1214 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1215 
proof(induct ys) 
1216 
case Nil thus ?case by simp 

1217 
next 

1218 
case (Cons y ys) 

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

1220 
proof cases 

1221 
assume Py: "P y" 

1222 
show ?thesis 

1223 
proof cases 

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

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

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

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

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

1229 
with Py Cons.prems show ?thesis by simp 
17629  1230 
qed 
1231 
next 

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

1232 
assume "\<not> P y" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

1233 
with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastforce 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

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

1235 
then show ?thesis .. 
17629  1236 
qed 
1237 
qed 

1238 

1239 
lemma filter_eq_ConsD: 

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

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

1242 
by(rule Cons_eq_filterD) simp 

1243 

1244 
lemma filter_eq_Cons_iff: 

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

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

1247 
by(auto dest:filter_eq_ConsD) 

1248 

1249 
lemma Cons_eq_filter_iff: 

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

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

1252 
by(auto dest:Cons_eq_filterD) 

1253 

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

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

1257 
apply(erule thin_rl) 

1258 
by (induct ys) simp_all 

1259 

15281  1260 

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

1261 
subsubsection {* List partitioning *} 
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 
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

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

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

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

1267 
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

1268 

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

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

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

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

1272 

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

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

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

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

1276 

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

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

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

1279 
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

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

1281 
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

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

1283 
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

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

1285 

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

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

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

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

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

1290 
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

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

1292 
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

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

1294 

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

1295 
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

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

1297 
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

1298 
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

1299 

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

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

1301 

35115  1302 

15392  1303 
subsubsection {* @{text concat} *} 
13114  1304 

13142  1305 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1306 
by (induct xs) auto 
13114  1307 

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

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

24308  1314 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1315 
by (induct xs) auto 
13114  1316 

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

1317 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1318 
by (induct xs) auto 
1319 

13142  1320 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1321 
by (induct xs) auto 
13114  1322 

13142 