author  bulwahn 
Mon, 30 Apr 2012 12:14:53 +0200  
changeset 47841  179b5e7c9803 
parent 47640  62bfba15b212 
child 48619  558e4e77ce69 
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 

47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

88 
primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

89 
where 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

90 
fold_Nil: "fold f [] = id" 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

91 
 fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x"  {* natural argument order *} 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

92 

d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

93 
primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

94 
where 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

95 
foldr_Nil: "foldr f [] = id" 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

96 
 foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs"  {* natural argument order *} 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

97 

d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

98 
primrec foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

99 
where 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

100 
foldl_Nil: "foldl f a [] = a" 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

101 
 foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs" 
34941  102 

103 
primrec 

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

105 
"concat [] = []" 

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

107 

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

112 
primrec 

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

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

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

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

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

118 

119 
primrec 

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

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

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

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

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

125 

126 
primrec 

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

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

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

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

131 

132 
primrec 

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

134 
"list_update [] i v = []" 

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

923  136 

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

137 
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

138 

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

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

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

144 

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

149 
primrec 

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

151 
"takeWhile P [] = []" 

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

153 

154 
primrec 

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

156 
"dropWhile P [] = []" 

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

158 

159 
primrec 

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

161 
"zip xs [] = []" 

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

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

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

165 

166 
primrec 

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

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

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

170 

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

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

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

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

174 

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

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

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

177 

47122  178 
primrec find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" where 
179 
"find _ [] = None" 

180 
 "find P (x#xs) = (if P x then Some x else find P xs)" 

181 

182 
hide_const (open) find 

183 

34941  184 
primrec 
185 
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

186 
"remove1 x [] = []" 

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

188 

189 
primrec 

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

191 
"removeAll x [] = []" 

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

193 

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

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

195 
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

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

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

198 

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

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

200 
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

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

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

203 

34941  204 
primrec 
205 
replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 

206 
replicate_0: "replicate 0 x = []" 

207 
 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

208 

13142  209 
text {* 
14589  210 
Function @{text size} is overloaded for all datatypes. Users may 
13366  211 
refer to the list version as @{text length}. *} 
13142  212 

19363  213 
abbreviation 
34941  214 
length :: "'a list \<Rightarrow> nat" where 
215 
"length \<equiv> size" 

15307  216 

46440
d4994e2e7364
use 'primrec' to define "rotate1", for uniformity (and to help firstorder tools that rely on "Spec_Rules")
blanchet
parents:
46439
diff
changeset

217 
primrec rotate1 :: "'a list \<Rightarrow> 'a list" where 
d4994e2e7364
use 'primrec' to define "rotate1", for uniformity (and to help firstorder tools that rely on "Spec_Rules")
blanchet
parents:
46439
diff
changeset

218 
"rotate1 [] = []"  
d4994e2e7364
use 'primrec' to define "rotate1", for uniformity (and to help firstorder tools that rely on "Spec_Rules")
blanchet
parents:
46439
diff
changeset

219 
"rotate1 (x # xs) = xs @ [x]" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

220 

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

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

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

224 

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

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

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

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

229 

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

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

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

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

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

234 
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

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

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

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

238 

26771  239 
text{* 
240 
\begin{figure}[htbp] 

241 
\fbox{ 

242 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

254 
@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\ 
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

255 
@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\ 
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

256 
@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\ 
27381  257 
@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\ 
258 
@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ 

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

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

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

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

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

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

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

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

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

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

269 
@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ 
35295  270 
@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\ 
47122  271 
@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\ 
272 
@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\ 

27381  273 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  274 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  275 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
276 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

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

46440
d4994e2e7364
use 'primrec' to define "rotate1", for uniformity (and to help firstorder tools that rely on "Spec_Rules")
blanchet
parents:
46439
diff
changeset

278 
@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\ 
d4994e2e7364
use 'primrec' to define "rotate1", for uniformity (and to help firstorder tools that rely on "Spec_Rules")
blanchet
parents:
46439
diff
changeset

279 
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\ 
40077  280 
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ 
281 
@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\ 

47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47131
diff
changeset

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

285 
\label{fig:Characteristic} 

286 
\end{figure} 

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

290 

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

293 

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

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

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

296 

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

297 
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

298 
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

299 
 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

300 

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

301 
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

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

303 
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

304 

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

305 
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

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

307 
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

308 

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

309 
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

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

311 
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

312 

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

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

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

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

316 
by simp_all 
24697  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 
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

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

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

321 

35195  322 
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

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

324 

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

325 
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

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

327 

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

328 
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

329 
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

330 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  331 

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

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

333 

24616  334 

23388  335 
subsubsection {* List comprehension *} 
23192  336 

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

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

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

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

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

343 

344 
The qualifiers after the dot are 

345 
\begin{description} 

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

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

347 
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

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

349 
%\item[local bindings] @ {text"let x = e"}. 
24349  350 
\end{description} 
23240  351 

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

352 
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

353 
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

354 
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

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

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

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

360 
definitions for the list comprehensions in question. *} 

361 

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

362 
nonterminal lc_qual and lc_quals 
23192  363 

364 
syntax 

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

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

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

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

368 
(*"_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

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

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

371 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  372 

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

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

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

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

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

378 
=> "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

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

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

381 
=> "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

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

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

384 
*) 
23240  385 

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

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

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

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

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

391 
parse_translation (advanced) {* 

46138
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 
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

394 
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

395 
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

396 
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

397 
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

398 

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

399 
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

400 

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

401 
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

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

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

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

405 
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

406 
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

407 
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

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

409 
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

410 
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

411 
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

412 
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

413 

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

414 
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

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

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

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

418 
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

419 
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

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

421 
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

422 
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

423 
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

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

425 
 _ => (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

426 

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

427 
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

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

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

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

431 
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

432 
 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

433 
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

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

435 
[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

436 
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

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

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

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

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

441 
[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

442 
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

443 
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

444 
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

445 

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

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

448 

42167  449 
ML {* 
450 
let 

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

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

453 
in 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

480 
end; 

481 
*} 

482 

35115  483 
(* 
24349  484 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  485 
*) 
486 

42167  487 

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

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

489 

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

490 
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

491 

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

492 
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

493 

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

494 
hide_const (open) coset 
35115  495 

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

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

497 

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

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

499 
"xs \<noteq> x # xs" 
13145  500 
by (induct xs) auto 
13114  501 

41697  502 
lemma not_Cons_self2 [simp]: 
503 
"x # xs \<noteq> xs" 

504 
by (rule not_Cons_self [symmetric]) 

13114  505 

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

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

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

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

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

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

517 
shows "P xs" 

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

519 
case Nil then show ?case by simp 

520 
next 

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

522 
case Nil with single show ?thesis by simp 

523 
next 

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

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

526 
ultimately show ?thesis by (rule cons) 

527 
qed 

528 
qed 

529 

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

13114  532 

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

533 
subsubsection {* @{const length} *} 
13114  534 

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

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

537 
append_eq_append_conv}. 
13142  538 
*} 
13114  539 

13142  540 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  541 
by (induct xs) auto 
13114  542 

13142  543 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  544 
by (induct xs) auto 
13114  545 

13142  546 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  547 
by (induct xs) auto 
13114  548 

13142  549 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  550 
by (cases xs) auto 
13114  551 

13142  552 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  553 
by (induct xs) auto 
13114  554 

13142  555 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  556 
by (induct xs) auto 
13114  557 

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

560 

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

13142  564 

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

14208  567 
apply (induct xs, simp, simp) 
14025  568 
apply blast 
569 
done 

570 

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

571 
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

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

573 

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

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

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

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

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

578 
proof (induct xs arbitrary: ys) 
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) then show ?case by (cases ys) simp_all 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

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

583 

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

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

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

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

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

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

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

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

591 
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

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

593 
qed 
13114  594 

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

595 
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

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

597 
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

598 
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

599 
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

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

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

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

603 
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

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

605 

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

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

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

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

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

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

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

612 
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

613 

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

614 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  615 
by (rule Eq_FalseI) auto 
24037  616 

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

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

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

619 
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

620 
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

621 
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

622 
*) 
24037  623 

624 
let 

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

625 

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

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

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

630 
 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

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

632 

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

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

636 
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

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

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

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

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

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

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

646 
in 
23214  647 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
648 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

653 

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

654 

15392  655 
subsubsection {* @{text "@"}  append *} 
13114  656 

13142  657 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  658 
by (induct xs) auto 
13114  659 

13142  660 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  661 
by (induct xs) auto 
3507  662 

13142  663 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  664 
by (induct xs) auto 
13114  665 

13142  666 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  667 
by (induct xs) auto 
13114  668 

13142  669 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  670 
by (induct xs) auto 
13114  671 

13142  672 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  673 
by (induct xs) auto 
13114  674 

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

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

677 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  678 
apply (induct xs arbitrary: ys) 
14208  679 
apply (case_tac ys, simp, force) 
680 
apply (case_tac ys, force, simp) 

13145  681 
done 
13142  682 

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

685 
apply (induct xs arbitrary: ys zs ts) 

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

686 
apply fastforce 
14495  687 
apply(case_tac zs) 
688 
apply simp 

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

689 
apply fastforce 
14495  690 
done 
691 

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

692 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  693 
by simp 
13142  694 

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

13145  696 
by simp 
13114  697 

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

698 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  699 
by simp 
13114  700 

13142  701 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  702 
using append_same_eq [of _ _ "[]"] by auto 
3507  703 

13142  704 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  705 
using append_same_eq [of "[]"] by auto 
13114  706 

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

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

13142  710 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  711 
by (induct xs) auto 
13114  712 

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

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

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

722 

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

725 
by(cases ys) auto 

726 

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

729 
by(cases ys) auto 

730 

14300  731 

13142  732 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  733 

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

13145  735 
by simp 
13114  736 

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

13114  740 

13142  741 
lemma append_eq_appendI: 
13145  742 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
743 
by (drule sym) simp 

13114  744 

745 

13142  746 
text {* 
13145  747 
Simplification procedure for all list equalities. 
748 
Currently only tries to rearrange @{text "@"} to see if 

749 
 both lists end in a singleton list, 

750 
 or both lists end in the same list. 

13142  751 
*} 
752 

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

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

758 
 last t = t; 

759 

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

761 
 list1 _ = false; 

762 

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

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

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

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

767 

768 
val rearr_ss = 

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

770 

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

13462  772 
let 
43594  773 
val lastl = last lhs and lastr = last rhs; 
774 
fun rearr conv = 

775 
let 

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

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

778 
val appT = [listT,listT] > listT 

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

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

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

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

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

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

785 
in 

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

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

788 
else NONE 

789 
end; 

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

13114  791 
*} 
792 

793 

15392  794 
subsubsection {* @{text map} *} 
13114  795 

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

796 
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

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

798 
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

799 

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

800 
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

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

802 
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

803 

13142  804 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  805 
by (induct xs) simp_all 
13114  806 

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

13142  810 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  811 
by (induct xs) auto 
13114  812 

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

813 
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

814 
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

815 

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

818 
apply(simp) 

819 
done 

820 

13142  821 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  822 
by (induct xs) auto 
13114  823 

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

826 

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

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

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

829 
by simp 
13114  830 

13142  831 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  832 
by (cases xs) auto 
13114  833 

13142  834 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  835 
by (cases xs) auto 
13114  836 

18447  837 
lemma map_eq_Cons_conv: 
14025  838 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  839 
by (cases xs) auto 
13114  840 

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

844 

18447  845 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
846 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

847 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

848 

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

18447  851 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  852 

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

853 
lemma map_eq_imp_length_eq: 
35510  854 
assumes "map f xs = map g ys" 
26734  855 
shows "length xs = length ys" 
856 
using assms proof (induct ys arbitrary: xs) 

857 
case Nil then show ?case by simp 

858 
next 

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

35510  860 
from Cons xs have "map f zs = map g ys" by simp 
26734  861 
moreover with Cons have "length zs = length ys" by blast 
862 
with xs show ?case by simp 

863 
qed 

864 

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

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

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

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

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

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

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

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

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

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

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

875 

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

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

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

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

879 

13114  880 
lemma map_injective: 
24526  881 
"map f xs = map f ys ==> inj f ==> xs = ys" 
882 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  883 

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

886 

13114  887 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  888 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  889 

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

14208  891 
apply (unfold inj_on_def, clarify) 
13145  892 
apply (erule_tac x = "[x]" in ballE) 
14208  893 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  894 
apply blast 
895 
done 

13114  896 

14339  897 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  898 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  899 

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

902 
apply(erule map_inj_on) 

903 
apply(blast intro:inj_onI dest:inj_onD) 

904 
done 

905 

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

13114  908 

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

909 
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

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

911 

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

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

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

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

915 

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

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

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

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

919 

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

920 
enriched_type map: map 
47122  921 
by (simp_all add: id_def) 
922 

923 
declare map.id[simp] 

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

924 

15392  925 
subsubsection {* @{text rev} *} 
13114  926 

13142  927 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  928 
by (induct xs) auto 
13114  929 

13142  930 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  931 
by (induct xs) auto 
13114  932 

15870  933 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
934 
by auto 

935 

13142  936 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  937 
by (induct xs) auto 
13114  938 

13142  939 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  940 
by (induct xs) auto 
13114  941 

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

944 

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

946 
by (cases xs) auto 

947 

46439
2388be11cb50
removed fact that confuses SPASS  better rely on "rev_rev_ident", which is stronger and more ATP friendly
blanchet
parents:
46424
diff
changeset

948 
lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)" 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

949 
apply (induct xs arbitrary: ys, force) 
14208  950 
apply (case_tac ys, simp, force) 
13145  951 
done 
13114  952 

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

955 

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

958 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  959 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
960 
done 

13114  961 

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

13145  964 
by (induct xs rule: rev_induct) auto 
13114  965 

13366  966 
lemmas rev_cases = rev_exhaust 
967 

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

970 

13114  971 

15392  972 
subsubsection {* @{text set} *} 
13114  973 

46698
f1dfcf8be88d
converting "set [...]" to "{...}" in evaluation results
nipkow
parents:
46669
diff
changeset

974 
declare set.simps [code_post] "pretty output" 
f1dfcf8be88d
converting "set [...]" to "{...}" in evaluation results
nipkow
parents:
46669
diff
changeset

975 

13142  976 
lemma finite_set [iff]: "finite (set xs)" 
13145  977 
by (induct xs) auto 
13114  978 

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

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

14099  984 

13142  985 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  986 
by auto 
13114  987 

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

990 

13142  991 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  992 
by (induct xs) auto 
13114  993 

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

996 

13142  997 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  998 
by (induct xs) auto 
13114  999 

13142  1000 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  1001 
by (induct xs) auto 
13114  1002 

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

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

1007 
by (induct j) auto 
13114  1008 

13142  1009 

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

1010 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  1011 
proof (induct xs) 
26073  1012 
case Nil thus ?case by simp 
1013 
next 

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

1015 
qed 

1016 

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

26073  1019 

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

1021 
proof (induct xs) 

1022 
case Nil thus ?case by simp 

18049  1023 
next 
1024 
case (Cons a xs) 

1025 
show ?case 

1026 
proof cases 

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

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

1029 
assume "x \<noteq> a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI) 
26073  1030 
qed 
1031 
qed 

1032 

1033 
lemma in_set_conv_decomp_first: 

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

26734  1035 
by (auto dest!: split_list_first) 
26073  1036 

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

1037 
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

1038 
proof (induct xs rule: rev_induct) 
26073  1039 
case Nil thus ?case by simp 
1040 
next 

1041 
case (snoc a xs) 

1042 
show ?case 

1043 
proof cases 

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

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

1046 
assume "x \<noteq> a" thus ?case using snoc by fastforce 
18049  1047 
qed 
1048 
qed 

1049 

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

26734  1052 
by (auto dest!: split_list_last) 
26073  1053 

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

1055 
proof (induct xs) 

1056 
case Nil thus ?case by simp 

1057 
next 

1058 
case Cons thus ?case 

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

1060 
qed 

1061 

1062 
lemma split_list_propE: 

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

1065 
using split_list_prop [OF assms] by blast 

26073  1066 

1067 
lemma split_list_first_prop: 

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

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

26734  1070 
proof (induct xs) 
26073  1071 
case Nil thus ?case by simp 
1072 
next 

1073 
case (Cons x xs) 

1074 
show ?case 

1075 
proof cases 

1076 
assume "P x" 

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

1077 
thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 
26073  1078 
next 
1079 
assume "\<not> P x" 

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

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

1082 
qed 

1083 
qed 

1084 

1085 
lemma split_list_first_propE: 

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

1088 
using split_list_first_prop [OF assms] by blast 

26073  1089 

1090 
lemma split_list_first_prop_iff: 

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

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

26734  1093 
by (rule, erule split_list_first_prop) auto 
26073  1094 

1095 
lemma split_list_last_prop: 

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

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

1098 
proof(induct xs rule:rev_induct) 

1099 
case Nil thus ?case by simp 

1100 
next 

1101 
case (snoc x xs) 

1102 
show ?case 

1103 
proof cases 

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

1105 
next 

1106 
assume "\<not> P x" 

1107 
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

1108 
thus ?thesis using `\<not> P x` snoc(1) by fastforce 
26073  1109 
qed 
1110 
qed 

1111 

1112 
lemma split_list_last_propE: 

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

1115 
using split_list_last_prop [OF assms] by blast 

26073  1116 

1117 
lemma split_list_last_prop_iff: 

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

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

26734  1120 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1121 

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

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

13508  1125 

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

13114  1128 

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

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

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

1131 
by (induct xs) auto 
15168  1132 

35115  1133 

15392  1134 
subsubsection {* @{text filter} *} 
13114  1135 

13142  1136 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1137 
by (induct xs) auto 
13114  1138 

15305  1139 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1140 
by (induct xs) simp_all 

1141 

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

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

1147 

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

1150 
by(induct xs) simp_all 

1151 

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

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

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

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

1162 
apply (induct xs) 

1163 
apply auto 

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

1165 
apply simp 

1166 
done 

13114  1167 

16965  1168 
lemma filter_map: 
1169 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1170 
by (induct xs) simp_all 

1171 

1172 
lemma length_filter_map[simp]: 

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

1174 
by (simp add:filter_map) 

1175 

13142  1176 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1177 
by auto 
13114  1178 

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

1181 
proof (induct xs) 

1182 
case Nil thus ?case by simp 

1183 
next 

1184 
case (Cons x xs) thus ?case 

1185 
apply (auto split:split_if_asm) 

1186 
using length_filter_le[of P xs] apply arith 

1187 
done 

1188 
qed 

13114  1189 

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

1192 
proof (induct xs) 

1193 
case Nil thus ?case by simp 

1194 
next 

1195 
case (Cons x xs) 

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

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

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

1199 
proof (cases) 

1200 
assume "p x" 

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

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

1209 
finally show ?thesis . 

1210 
next 

1211 
assume "\<not> p x" 

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

25162  1213 
by(auto simp add: image_def split:nat.split elim:lessE) 
15281  1214 
have "length (filter p (x # xs)) = card ?S" 
23388  1215 
using Cons `\<not> p x` by simp 
15281  1216 
also have "\<dots> = card(Suc ` ?S)" using fin 
44921  1217 
by (simp add: card_image) 
15281  1218 
also have "\<dots> = card ?S'" using eq fin 
1219 
by (simp add:card_insert_if) 

1220 
finally show ?thesis . 

1221 
qed 

1222 
qed 

1223 

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

1226 
\<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  1227 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1228 
proof(induct ys) 
1229 
case Nil thus ?case by simp 

1230 
next 

1231 
case (Cons y ys) 

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

1233 
proof cases 

1234 
assume Py: "P y" 

1235 
show ?thesis 

1236 
proof cases 

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

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

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

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

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

1242 
with Py Cons.prems show ?thesis by simp 
17629  1243 
qed 
1244 
next 

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

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

1246 
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

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

1248 
then show ?thesis .. 
17629  1249 
qed 
1250 
qed 

1251 

1252 
lemma filter_eq_ConsD: 

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

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

1255 
by(rule Cons_eq_filterD) simp 

1256 

1257 
lemma filter_eq_Cons_iff: 

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

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

1260 
by(auto dest:filter_eq_ConsD) 

1261 

1262 
lemma Cons_eq_filter_iff: 

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

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

1265 
by(auto dest:Cons_eq_filterD) 

1266 

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

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

1270 
apply(erule thin_rl) 

1271 
by (induct ys) simp_all 

1272 

15281  1273 

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

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

1275 

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

1276 
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

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

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

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

1280 
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

1281 

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

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

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

1284 
by (induct xs) (auto simp add: Let_def split_def) 
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_filter2: 
57fb6a8b099e
restructuring; explicit case names for rule list_induct2
haftmann
parents:
26300
diff
changeset

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

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

1289 

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

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

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

1292 
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

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

1294 
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

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

1296 
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

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

1298 

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

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

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

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

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

1303 
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

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

1305 
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

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

1307 

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

1308 
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

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

1310 
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

1311 
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

1312 

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

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

1314 

35115  1315 

15392  1316 
subsubsection {* @{text concat} *} 
13114  1317 

13142  1318 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1319 
by (induct xs) auto 
13114  1320 

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