author  bulwahn 
Thu, 08 Nov 2012 11:59:48 +0100  
changeset 50027  7747a9f4c358 
parent 49963  326f87427719 
child 50134  13211e07d931 
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 
15131  9 
begin 
923  10 

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

923  14 

34941  15 
syntax 
16 
 {* list Enumeration *} 

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

19 
translations 

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

21 
"[x]" == "x#[]" 

22 

35115  23 

24 
subsection {* Basic list processing functions *} 

15302  25 

34941  26 
primrec 
27 
hd :: "'a list \<Rightarrow> 'a" where 

28 
"hd (x # xs) = x" 

29 

30 
primrec 

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

32 
"tl [] = []" 

33 
 "tl (x # xs) = xs" 

34 

35 
primrec 

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

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

38 

39 
primrec 

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

41 
"butlast []= []" 

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

43 

44 
primrec 

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

46 
"set [] = {}" 

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

48 

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

49 
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

50 
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

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

52 

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

55 
"map f [] = []" 

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

57 

58 
primrec 

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

60 
append_Nil:"[] @ ys = ys" 

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

62 

63 
primrec 

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

65 
"rev [] = []" 

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

67 

68 
primrec 

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

70 
"filter P [] = []" 

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

72 

73 
syntax 

74 
 {* Special syntax for filter *} 

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

77 
translations 

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

79 

80 
syntax (xsymbols) 

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

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

85 
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

86 
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

87 
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

88 
 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

89 

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

91 
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

92 
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

93 
 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

94 

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

96 
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

97 
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

98 
 foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs" 
34941  99 

100 
primrec 

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

102 
"concat [] = []" 

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

104 

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

109 
primrec 

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

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

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

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

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

115 

116 
primrec 

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

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

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

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

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

122 

123 
primrec 

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

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

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

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

128 

129 
primrec 

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

131 
"list_update [] i v = []" 

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

923  133 

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

134 
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

135 

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

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

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

141 

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

146 
primrec 

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

148 
"takeWhile P [] = []" 

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

150 

151 
primrec 

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

153 
"dropWhile P [] = []" 

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

155 

156 
primrec 

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

158 
"zip xs [] = []" 

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

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

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

162 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

163 
primrec 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

164 
product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

165 
"product [] _ = []" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

166 
 "product (x#xs) ys = map (Pair x) ys @ product xs ys" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

167 

744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

168 
hide_const (open) product 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

169 

34941  170 
primrec 
171 
upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where 

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

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

174 

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

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

176 
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

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

178 

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

179 
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

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

181 

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

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

185 

186 
hide_const (open) find 

187 

34941  188 
primrec 
189 
remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

190 
"remove1 x [] = []" 

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

192 

193 
primrec 

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

195 
"removeAll x [] = []" 

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

197 

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

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

199 
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

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

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

202 

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

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

204 
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

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

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

207 

34941  208 
primrec 
209 
replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 

210 
replicate_0: "replicate 0 x = []" 

211 
 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

212 

13142  213 
text {* 
14589  214 
Function @{text size} is overloaded for all datatypes. Users may 
13366  215 
refer to the list version as @{text length}. *} 
13142  216 

19363  217 
abbreviation 
34941  218 
length :: "'a list \<Rightarrow> nat" where 
219 
"length \<equiv> size" 

15307  220 

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

221 
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

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

223 
"rotate1 (x # xs) = xs @ [x]" 
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 
rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
30971  227 
"rotate n = rotate1 ^^ n" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

228 

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

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

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

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

233 

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

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

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

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

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

238 
primrec 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

239 
sublists :: "'a list \<Rightarrow> 'a list list" where 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

240 
"sublists [] = [[]]" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

241 
 "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

242 

744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

243 
primrec 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

244 
n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

245 
"n_lists 0 xs = [[]]" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

246 
 "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

247 

744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

248 
hide_const (open) n_lists 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

249 

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

250 
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

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

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

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

254 

26771  255 
text{* 
256 
\begin{figure}[htbp] 

257 
\fbox{ 

258 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

275 
@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\ 
27381  276 
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ 
277 
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ 

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

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

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

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

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

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

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

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

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

27381  290 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  291 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  292 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
293 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

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

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

295 
@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\ 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

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

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

298 
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\ 
40077  299 
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ 
300 
@{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

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

304 
\label{fig:Characteristic} 

305 
\end{figure} 

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

309 

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

312 

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

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

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

315 

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

316 
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

317 
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

318 
 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

319 

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

320 
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

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

322 
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

323 

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

324 
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

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

326 
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

327 

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

328 
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

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

330 
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

331 

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

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

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

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

335 
by simp_all 
24697  336 

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

337 
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

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

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

340 

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

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

343 

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

344 
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

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

346 

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

347 
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

348 
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

349 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  350 

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

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

352 

24616  353 

23388  354 
subsubsection {* List comprehension *} 
23192  355 

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

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

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

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

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

362 

363 
The qualifiers after the dot are 

364 
\begin{description} 

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

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

366 
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

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

368 
%\item[local bindings] @ {text"let x = e"}. 
24349  369 
\end{description} 
23240  370 

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

371 
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

372 
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

373 
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

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

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

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

379 
definitions for the list comprehensions in question. *} 

380 

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

381 
nonterminal lc_qual and lc_quals 
23192  382 

383 
syntax 

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

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

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

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

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

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

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

390 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  391 

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

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

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

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

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

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

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

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

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

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

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

403 
*) 
23240  404 

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

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

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

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

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

410 
parse_translation (advanced) {* 

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

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

412 
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

413 
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

414 
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

415 
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

416 
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

417 

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

418 
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

419 

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

420 
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

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

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

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

424 
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

425 
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

426 
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

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

428 
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

429 
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

430 
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

431 
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

432 

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

433 
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

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

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

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

437 
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

438 
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

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

440 
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

441 
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

442 
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

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

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

445 

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

446 
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

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

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

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

450 
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

451 
 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

452 
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

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

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

455 
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

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

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

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

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

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

461 
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

462 
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

463 
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

464 

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

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

467 

42167  468 
ML {* 
469 
let 

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

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

472 
in 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

499 
end; 

500 
*} 

501 

35115  502 
(* 
24349  503 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  504 
*) 
505 

42167  506 

48891  507 
ML_file "Tools/list_to_set_comprehension.ML" 
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

508 

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

509 
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

510 

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

511 
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

512 

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

513 
hide_const (open) coset 
35115  514 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

515 

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

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

517 

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

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

519 
"xs \<noteq> x # xs" 
13145  520 
by (induct xs) auto 
13114  521 

41697  522 
lemma not_Cons_self2 [simp]: 
523 
"x # xs \<noteq> xs" 

524 
by (rule not_Cons_self [symmetric]) 

13114  525 

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

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

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

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

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

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

537 
shows "P xs" 

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

539 
case Nil then show ?case by simp 

540 
next 

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

542 
case Nil with single show ?thesis by simp 

543 
next 

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

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

546 
ultimately show ?thesis by (rule cons) 

547 
qed 

548 
qed 

549 

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

13114  552 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

553 

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

554 
subsubsection {* @{const length} *} 
13114  555 

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

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

558 
append_eq_append_conv}. 
13142  559 
*} 
13114  560 

13142  561 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  562 
by (induct xs) auto 
13114  563 

13142  564 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  565 
by (induct xs) auto 
13114  566 

13142  567 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  568 
by (induct xs) auto 
13114  569 

13142  570 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  571 
by (cases xs) auto 
13114  572 

13142  573 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  574 
by (induct xs) auto 
13114  575 

13142  576 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  577 
by (induct xs) auto 
13114  578 

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

581 

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

13142  585 

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

14208  588 
apply (induct xs, simp, simp) 
14025  589 
apply blast 
590 
done 

591 

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

592 
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

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

594 

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

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

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

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

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

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

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

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

602 
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

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

604 

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

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

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

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

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

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

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

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

612 
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

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

614 
qed 
13114  615 

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

616 
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

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

618 
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

619 
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

620 
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

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

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

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

624 
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

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

626 

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

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

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

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

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

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

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

633 
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

634 

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

635 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  636 
by (rule Eq_FalseI) auto 
24037  637 

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

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

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

640 
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

641 
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

642 
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

643 
*) 
24037  644 

645 
let 

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

646 

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

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

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

651 
 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

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

653 

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

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

657 
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

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

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

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

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

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

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

667 
in 
23214  668 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
669 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

674 

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

675 

15392  676 
subsubsection {* @{text "@"}  append *} 
13114  677 

13142  678 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  679 
by (induct xs) auto 
13114  680 

13142  681 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  682 
by (induct xs) auto 
3507  683 

13142  684 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  685 
by (induct xs) auto 
13114  686 

13142  687 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  688 
by (induct xs) auto 
13114  689 

13142  690 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  691 
by (induct xs) auto 
13114  692 

13142  693 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  694 
by (induct xs) auto 
13114  695 

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

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

698 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  699 
apply (induct xs arbitrary: ys) 
14208  700 
apply (case_tac ys, simp, force) 
701 
apply (case_tac ys, force, simp) 

13145  702 
done 
13142  703 

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

706 
apply (induct xs arbitrary: ys zs ts) 

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

707 
apply fastforce 
14495  708 
apply(case_tac zs) 
709 
apply simp 

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

710 
apply fastforce 
14495  711 
done 
712 

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

713 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  714 
by simp 
13142  715 

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

13145  717 
by simp 
13114  718 

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

719 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  720 
by simp 
13114  721 

13142  722 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  723 
using append_same_eq [of _ _ "[]"] by auto 
3507  724 

13142  725 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  726 
using append_same_eq [of "[]"] by auto 
13114  727 

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

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

13142  731 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  732 
by (induct xs) auto 
13114  733 

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

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

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

743 

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

746 
by(cases ys) auto 

747 

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

750 
by(cases ys) auto 

751 

14300  752 

13142  753 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  754 

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

13145  756 
by simp 
13114  757 

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

13114  761 

13142  762 
lemma append_eq_appendI: 
13145  763 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
764 
by (drule sym) simp 

13114  765 

766 

13142  767 
text {* 
13145  768 
Simplification procedure for all list equalities. 
769 
Currently only tries to rearrange @{text "@"} to see if 

770 
 both lists end in a singleton list, 

771 
 or both lists end in the same list. 

13142  772 
*} 
773 

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

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

779 
 last t = t; 

780 

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

782 
 list1 _ = false; 

783 

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

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

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

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

788 

789 
val rearr_ss = 

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

791 

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

13462  793 
let 
43594  794 
val lastl = last lhs and lastr = last rhs; 
795 
fun rearr conv = 

796 
let 

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

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

799 
val appT = [listT,listT] > listT 

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

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

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

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

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

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

806 
in 

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

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

809 
else NONE 

810 
end; 

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

13114  812 
*} 
813 

814 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

815 
subsubsection {* @{const map} *} 
13114  816 

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

817 
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

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

819 
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

820 

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

821 
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

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

823 
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

824 

13142  825 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  826 
by (induct xs) simp_all 
13114  827 

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

13142  831 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  832 
by (induct xs) auto 
13114  833 

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

834 
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

835 
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

836 

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

839 
apply(simp) 

840 
done 

841 

13142  842 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  843 
by (induct xs) auto 
13114  844 

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

847 

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

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

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

850 
by simp 
13114  851 

13142  852 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  853 
by (cases xs) auto 
13114  854 

13142  855 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  856 
by (cases xs) auto 
13114  857 

18447  858 
lemma map_eq_Cons_conv: 
14025  859 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  860 
by (cases xs) auto 
13114  861 

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

865 

18447  866 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
867 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

868 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

869 

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

18447  872 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  873 

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

874 
lemma map_eq_imp_length_eq: 
35510  875 
assumes "map f xs = map g ys" 
26734  876 
shows "length xs = length ys" 
877 
using assms proof (induct ys arbitrary: xs) 

878 
case Nil then show ?case by simp 

879 
next 

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

35510  881 
from Cons xs have "map f zs = map g ys" by simp 
26734  882 
moreover with Cons have "length zs = length ys" by blast 
883 
with xs show ?case by simp 

884 
qed 

885 

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

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

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

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

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

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

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

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

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

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

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

896 

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

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

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

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

900 

13114  901 
lemma map_injective: 
24526  902 
"map f xs = map f ys ==> inj f ==> xs = ys" 
903 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  904 

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

907 

13114  908 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  909 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  910 

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

14208  912 
apply (unfold inj_on_def, clarify) 
13145  913 
apply (erule_tac x = "[x]" in ballE) 
14208  914 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  915 
apply blast 
916 
done 

13114  917 

14339  918 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  919 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  920 

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

923 
apply(erule map_inj_on) 

924 
apply(blast intro:inj_onI dest:inj_onD) 

925 
done 

926 

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

13114  929 

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

930 
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

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

932 

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

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

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

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

936 

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

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

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

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

940 

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

941 
enriched_type map: map 
47122  942 
by (simp_all add: id_def) 
943 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

944 
declare map.id [simp] 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

945 

744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

946 

744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

947 
subsubsection {* @{const rev} *} 
13114  948 

13142  949 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  950 
by (induct xs) auto 
13114  951 

13142  952 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  953 
by (induct xs) auto 
13114  954 

15870  955 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
956 
by auto 

957 

13142  958 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  959 
by (induct xs) auto 
13114  960 

13142  961 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  962 
by (induct xs) auto 
13114  963 

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

966 

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

968 
by (cases xs) auto 

969 

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

970 
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

971 
apply (induct xs arbitrary: ys, force) 
14208  972 
apply (case_tac ys, simp, force) 
13145  973 
done 
13114  974 

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

977 

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

980 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  981 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
982 
done 

13114  983 

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

13145  986 
by (induct xs rule: rev_induct) auto 
13114  987 

13366  988 
lemmas rev_cases = rev_exhaust 
989 

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

992 

13114  993 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

994 
subsubsection {* @{const set} *} 
13114  995 

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

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

997 

13142  998 
lemma finite_set [iff]: "finite (set xs)" 
13145  999 
by (induct xs) auto 
13114  1000 

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

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

14099  1006 

13142  1007 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  1008 
by auto 
13114  1009 

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

1012 

13142  1013 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  1014 
by (induct xs) auto 
13114  1015 

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

1018 

13142  1019 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  1020 
by (induct xs) auto 
13114  1021 

13142  1022 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  1023 
by (induct xs) auto 
13114  1024 

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

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

1029 
by (induct j) auto 
13114  1030 

13142  1031 

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

1032 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  1033 
proof (induct xs) 
26073  1034 
case Nil thus ?case by simp 
1035 
next 

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

1037 
qed 

1038 

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

26073  1041 

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

1043 
proof (induct xs) 

1044 
case Nil thus ?case by simp 

18049  1045 
next 
1046 
case (Cons a xs) 

1047 
show ?case 

1048 
proof cases 

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

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

1051 
assume "x \<noteq> a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI) 
26073  1052 
qed 
1053 
qed 

1054 

1055 
lemma in_set_conv_decomp_first: 

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

26734  1057 
by (auto dest!: split_list_first) 
26073  1058 

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

1059 
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

1060 
proof (induct xs rule: rev_induct) 
26073  1061 
case Nil thus ?case by simp 
1062 
next 

1063 
case (snoc a xs) 

1064 
show ?case 

1065 
proof cases 

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

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

1068 
assume "x \<noteq> a" thus ?case using snoc by fastforce 
18049  1069 
qed 
1070 
qed 

1071 

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

26734  1074 
by (auto dest!: split_list_last) 
26073  1075 

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

1077 
proof (induct xs) 

1078 
case Nil thus ?case by simp 

1079 
next 

1080 
case Cons thus ?case 

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

1082 
qed 

1083 

1084 
lemma split_list_propE: 

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

1087 
using split_list_prop [OF assms] by blast 

26073  1088 

1089 
lemma split_list_first_prop: 

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

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

26734  1092 
proof (induct xs) 
26073  1093 
case Nil thus ?case by simp 
1094 
next 

1095 
case (Cons x xs) 

1096 
show ?case 

1097 
proof cases 

1098 
assume "P x" 

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

1099 
thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append) 
26073  1100 
next 
1101 
assume "\<not> P x" 

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

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

1104 
qed 

1105 
qed 

1106 

1107 
lemma split_list_first_propE: 

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

1110 
using split_list_first_prop [OF assms] by blast 

26073  1111 

1112 
lemma split_list_first_prop_iff: 

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

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

26734  1115 
by (rule, erule split_list_first_prop) auto 
26073  1116 

1117 
lemma split_list_last_prop: 

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

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

1120 
proof(induct xs rule:rev_induct) 

1121 
case Nil thus ?case by simp 

1122 
next 

1123 
case (snoc x xs) 

1124 
show ?case 

1125 
proof cases 

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

1127 
next 

1128 
assume "\<not> P x" 

1129 
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

1130 
thus ?thesis using `\<not> P x` snoc(1) by fastforce 
26073  1131 
qed 
1132 
qed 

1133 

1134 
lemma split_list_last_propE: 

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

1137 
using split_list_last_prop [OF assms] by blast 

26073  1138 

1139 
lemma split_list_last_prop_iff: 

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

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

26734  1142 
by (metis split_list_last_prop [where P=P] in_set_conv_decomp) 
26073  1143 

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

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

13508  1147 

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

13114  1150 

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

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

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

1153 
by (induct xs) auto 
15168  1154 

35115  1155 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

1156 
subsubsection {* @{const filter} *} 
13114  1157 

13142  1158 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  1159 
by (induct xs) auto 
13114  1160 

15305  1161 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
1162 
by (induct xs) simp_all 

1163 

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

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

1169 

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

1172 
by(induct xs) simp_all 

1173 

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

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

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

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

1184 
apply (induct xs) 

1185 
apply auto 

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

1187 
apply simp 

1188 
done 

13114  1189 

16965  1190 
lemma filter_map: 
1191 
"filter P (map f xs) = map f (filter (P o f) xs)" 

1192 
by (induct xs) simp_all 

1193 

1194 
lemma length_filter_map[simp]: 

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

1196 
by (simp add:filter_map) 

1197 

13142  1198 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  1199 
by auto 
13114  1200 

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

1203 
proof (induct xs) 

1204 
case Nil thus ?case by simp 

1205 
next 

1206 
case (Cons x xs) thus ?case 

1207 
apply (auto split:split_if_asm) 

1208 
using length_filter_le[of P xs] apply arith 

1209 
done 

1210 
qed 

13114  1211 

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

1214 
proof (induct xs) 

1215 
case Nil thus ?case by simp 

1216 
next 

1217 
case (Cons x xs) 

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

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

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

1221 
proof (cases) 

1222 
assume "p x" 

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

25162  1224 
by(auto simp: image_def split:nat.split dest:gr0_implies_Suc) 
15281  1225 
have "length (filter p (x # xs)) = Suc(card ?S)" 
23388  1226 
using Cons `p x` by simp 
15281  1227 
also have "\<dots> = Suc(card(Suc ` ?S))" using fin 
44921  1228 
by (simp add: card_image) 
15281  1229 
also have "\<dots> = card ?S'" using eq fin 
1230 
by (simp add:card_insert_if) (simp add:image_def) 

1231 
finally show ?thesis . 

1232 
next 

1233 
assume "\<not> p x" 

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

25162  1235 
by(auto simp add: image_def split:nat.split elim:lessE) 
15281  1236 
have "length (filter p (x # xs)) = card ?S" 
23388  1237 
using Cons `\<not> p x` by simp 
15281  1238 
also have "\<dots> = card(Suc ` ?S)" using fin 
44921  1239 
by (simp add: card_image) 
15281  1240 
also have "\<dots> = card ?S'" using eq fin 
1241 
by (simp add:card_insert_if) 

1242 
finally show ?thesis . 

1243 
qed 

1244 
qed 

1245 

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

1248 
\<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  1249 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  1250 
proof(induct ys) 
1251 
case Nil thus ?case by simp 

1252 
next 

1253 
case (Cons y ys) 

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

1255 
proof cases 

1256 
assume Py: "P y" 

1257 
show ?thesis 

1258 
proof cases 

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

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

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

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

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

1264 
with Py Cons.prems show ?thesis by simp 
17629  1265 
qed 
1266 
next 

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

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

1268 
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

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

1270 
then show ?thesis .. 
17629  1271 
qed 
1272 
qed 

1273 

1274 
lemma filter_eq_ConsD: 

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

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

1277 
by(rule Cons_eq_filterD) simp 

1278 

1279 
lemma filter_eq_Cons_iff: 

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

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

1282 
by(auto dest:filter_eq_ConsD) 

1283 

1284 
lemma Cons_eq_filter_iff: 

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

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

1287 
by(auto dest:Cons_eq_filterD) 

1288 

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

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

1292 
apply(erule thin_rl) 

1293 
by (induct ys) simp_all 

1294 

15281  1295 

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

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

1297 

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

1298 
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

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

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

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

1302 
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

1303 

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

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

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

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

1307 

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

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

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

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

1311 

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

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

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

1314 
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

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

1316 
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

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

1318 
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

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

1320 

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

1321 
lemma partition_set: 