author  wenzelm 
Thu, 30 Apr 2015 15:58:15 +0200  
changeset 60159  879918f4ee0f 
parent 60158  6696fc3f3347 
child 60160  52aa014308cb 
permissions  rwrr 
13462  1 
(* Title: HOL/List.thy 
2 
Author: Tobias Nipkow 

923  3 
*) 
4 

58889  5 
section {* The datatype of finite lists *} 
13122  6 

15131  7 
theory List 
58916  8 
imports Sledgehammer Code_Numeral Lifting_Set 
15131  9 
begin 
923  10 

58310  11 
datatype (set: 'a) list = 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57198
diff
changeset

12 
Nil ("[]") 
55405
0a155051bd9d
use new selector support to define 'the', 'hd', 'tl'
blanchet
parents:
55404
diff
changeset

13 
 Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) 
57206
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57200
diff
changeset

14 
for 
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57200
diff
changeset

15 
map: map 
d9be905d6283
changed syntax of map: and rel: arguments to BNFbased datatypes
blanchet
parents:
57200
diff
changeset

16 
rel: list_all2 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57198
diff
changeset

17 
where 
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57198
diff
changeset

18 
"tl [] = []" 
57123
b5324647e0f1
tuned whitespace, to make datatype definitions slightly less intimidating
blanchet
parents:
57091
diff
changeset

19 

55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55525
diff
changeset

20 
datatype_compat list 
55404
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

21 

55406  22 
lemma [case_names Nil Cons, cases type: list]: 
23 
 {* for backward compatibility  names of variables differ *} 

24 
"(y = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>a list. y = a # list \<Longrightarrow> P) \<Longrightarrow> P" 

25 
by (rule list.exhaust) 

26 

27 
lemma [case_names Nil Cons, induct type: list]: 

28 
 {* for backward compatibility  names of variables differ *} 

29 
"P [] \<Longrightarrow> (\<And>a list. P list \<Longrightarrow> P (a # list)) \<Longrightarrow> P list" 

30 
by (rule list.induct) 

31 

55442  32 
text {* Compatibility: *} 
33 

55404
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

34 
setup {* Sign.mandatory_path "list" *} 
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

35 

5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

36 
lemmas inducts = list.induct 
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

37 
lemmas recs = list.rec 
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

38 
lemmas cases = list.case 
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

39 

5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

40 
setup {* Sign.parent_path *} 
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

41 

57816
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
57599
diff
changeset

42 
lemmas set_simps = list.set (* legacy *) 
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
57599
diff
changeset

43 

34941  44 
syntax 
45 
 {* list Enumeration *} 

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

48 
translations 

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

50 
"[x]" == "x#[]" 

51 

35115  52 

53 
subsection {* Basic list processing functions *} 

15302  54 

58135  55 
primrec (nonexhaustive) last :: "'a list \<Rightarrow> 'a" where 
50548  56 
"last (x # xs) = (if xs = [] then x else last xs)" 
57 

58 
primrec butlast :: "'a list \<Rightarrow> 'a list" where 

57816
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
57599
diff
changeset

59 
"butlast [] = []"  
50548  60 
"butlast (x # xs) = (if xs = [] then [] else x # butlast xs)" 
61 

55584  62 
lemma set_rec: "set xs = rec_list {} (\<lambda>x _. insert x) xs" 
63 
by (induct xs) auto 

50548  64 

65 
definition coset :: "'a list \<Rightarrow> 'a set" where 

66 
[simp]: "coset xs =  set xs" 

67 

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

69 
append_Nil: "[] @ ys = ys"  

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

71 

72 
primrec rev :: "'a list \<Rightarrow> 'a list" where 

73 
"rev [] = []"  

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

75 

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

77 
"filter P [] = []"  

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

34941  79 

80 
syntax 

81 
 {* Special syntax for filter *} 

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

84 
translations 

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

86 

87 
syntax (xsymbols) 

35115  88 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  89 
syntax (HTML output) 
35115  90 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  91 

50548  92 
primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where 
93 
fold_Nil: "fold f [] = id"  

94 
fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x" 

95 

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

97 
foldr_Nil: "foldr f [] = id"  

98 
foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs" 

99 

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

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

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

103 

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

105 
"concat [] = []"  

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

107 

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

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

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

34941  111 
 {*Warning: simpset does not contain this definition, but separate 
112 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

113 

50548  114 
primrec take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
115 
take_Nil:"take n [] = []"  

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

34941  117 
 {*Warning: simpset does not contain this definition, but separate 
118 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

119 

58135  120 
primrec (nonexhaustive) nth :: "'a list => nat => 'a" (infixl "!" 100) where 
50548  121 
nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x  Suc k \<Rightarrow> xs ! k)" 
34941  122 
 {*Warning: simpset does not contain this definition, but separate 
123 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

124 

50548  125 
primrec list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 
126 
"list_update [] i v = []"  

127 
"list_update (x # xs) i v = 

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

923  129 

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

130 
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

131 

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

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

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

137 

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

50548  142 
primrec takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
143 
"takeWhile P [] = []"  

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

145 

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

147 
"dropWhile P [] = []"  

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

149 

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

151 
"zip xs [] = []"  

152 
zip_Cons: "zip xs (y # ys) = 

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

34941  154 
 {*Warning: simpset does not contain this definition, but separate 
155 
theorems for @{text "xs = []"} and @{text "xs = z # zs"} *} 

156 

50548  157 
primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where 
158 
"product [] _ = []"  

159 
"product (x#xs) ys = map (Pair x) ys @ product xs ys" 

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

160 

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

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

162 

53721
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

163 
primrec product_lists :: "'a list list \<Rightarrow> 'a list list" where 
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

164 
"product_lists [] = [[]]"  
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

165 
"product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) xs)" 
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

166 

50548  167 
primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where 
168 
upt_0: "[i..<0] = []"  

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

170 

171 
definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

172 
"insert x xs = (if x \<in> set xs then xs else x # xs)" 

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

173 

57198  174 
definition union :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
175 
"union = fold insert" 

176 

177 
hide_const (open) insert union 

178 
hide_fact (open) insert_def union_def 

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

179 

47122  180 
primrec find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" where 
50548  181 
"find _ [] = None"  
182 
"find P (x#xs) = (if P x then Some x else find P xs)" 

47122  183 

184 
hide_const (open) find 

185 

59728  186 
primrec count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where 
187 
"count [] y = 0"  

188 
"count (x#xs) y = (if x=y then count xs y + 1 else count xs y)" 

189 

190 
hide_const (open) count 

191 

55807  192 
definition 
193 
"extract" :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> ('a list * 'a * 'a list) option" 

194 
where "extract P xs = 

195 
(case dropWhile (Not o P) xs of 

196 
[] \<Rightarrow> None  

197 
y#ys \<Rightarrow> Some(takeWhile (Not o P) xs, y, ys))" 

198 

199 
hide_const (open) "extract" 

200 

51096  201 
primrec those :: "'a option list \<Rightarrow> 'a list option" 
202 
where 

203 
"those [] = Some []"  

204 
"those (x # xs) = (case x of 

205 
None \<Rightarrow> None 

55466  206 
 Some y \<Rightarrow> map_option (Cons y) (those xs))" 
51096  207 

50548  208 
primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
209 
"remove1 x [] = []"  

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

211 

212 
primrec removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

213 
"removeAll x [] = []"  

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

215 

216 
primrec distinct :: "'a list \<Rightarrow> bool" where 

217 
"distinct [] \<longleftrightarrow> True"  

218 
"distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs" 

219 

220 
primrec remdups :: "'a list \<Rightarrow> 'a list" where 

221 
"remdups [] = []"  

222 
"remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)" 

223 

53721
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

224 
fun remdups_adj :: "'a list \<Rightarrow> 'a list" where 
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

225 
"remdups_adj [] = []"  
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

226 
"remdups_adj [x] = [x]"  
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

227 
"remdups_adj (x # y # xs) = (if x = y then remdups_adj (x # xs) else x # remdups_adj (y # xs))" 
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

228 

50548  229 
primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where 
230 
replicate_0: "replicate 0 x = []"  

231 
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

232 

13142  233 
text {* 
14589  234 
Function @{text size} is overloaded for all datatypes. Users may 
13366  235 
refer to the list version as @{text length}. *} 
13142  236 

50548  237 
abbreviation length :: "'a list \<Rightarrow> nat" where 
238 
"length \<equiv> size" 

15307  239 

51173  240 
definition enumerate :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where 
241 
enumerate_eq_zip: "enumerate n xs = zip [n..<n + length xs] xs" 

242 

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

243 
primrec rotate1 :: "'a list \<Rightarrow> 'a list" where 
50548  244 
"rotate1 [] = []"  
245 
"rotate1 (x # xs) = xs @ [x]" 

246 

247 
definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

248 
"rotate n = rotate1 ^^ n" 

249 

250 
definition sublist :: "'a list => nat set => 'a list" where 

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

252 

253 
primrec sublists :: "'a list \<Rightarrow> 'a list list" where 

254 
"sublists [] = [[]]"  

255 
"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" 

256 

257 
primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where 

258 
"n_lists 0 xs = [[]]"  

259 
"n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))" 

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

260 

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

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

262 

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

263 
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

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

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

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

267 

26771  268 
text{* 
269 
\begin{figure}[htbp] 

270 
\fbox{ 

271 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

51173  288 
@{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\ 
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

289 
@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\ 
53721
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

290 
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\ 
27381  291 
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ 
292 
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ 

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

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

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

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

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

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

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

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

53721
ccaceea6c768
added two functions to List (one contributed by Manuel Eberl)
traytel
parents:
53689
diff
changeset

301 
@{lemma "remdups_adj [2,2,3,1,1::nat,2,1] = [2,3,1,2,1]" by simp}\\ 
34978
874150ddd50a
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
haftmann
parents:
34942
diff
changeset

302 
@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ 
35295  303 
@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\ 
57198  304 
@{lemma "List.union [2,3,4] [0::int,1,2] = [4,3,0,1,2]" by (simp add: List.insert_def List.union_def)}\\ 
47122  305 
@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\ 
306 
@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\ 

59728  307 
@{lemma "List.count [0,1,0,2::int] 0 = 2" by (simp)}\\ 
55807  308 
@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\ 
309 
@{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\ 

27381  310 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  311 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  312 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
313 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

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

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

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

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

318 
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\ 
40077  319 
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ 
58101  320 
@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)} 
26771  321 
\end{tabular}} 
322 
\caption{Characteristic examples} 

323 
\label{fig:Characteristic} 

324 
\end{figure} 

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

328 

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

331 

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

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

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

334 

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

335 
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

336 
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

337 
 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

338 

58807  339 
lemma sorted_single [iff]: "sorted [x]" 
340 
by (rule sorted.Cons) auto 

341 

342 
lemma sorted_many: "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)" 

343 
by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto) 

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

344 

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

345 
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

346 
"sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)" 
58807  347 
by (auto intro: sorted_many elim: sorted.cases) 
39915
ecf97cf3d248
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
haftmann
parents:
39774
diff
changeset

348 

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

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

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

351 
"sorted [x] \<longleftrightarrow> True" 
58807  352 
by simp_all 
24697  353 

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

354 
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
50548  355 
"insort_key f x [] = [x]"  
356 
"insort_key f x (y#ys) = 

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

358 

35195  359 
definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
50548  360 
"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

361 

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

362 
definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
50548  363 
"insort_insert_key f x xs = 
364 
(if f x \<in> f ` set xs then xs else insort_key f x xs)" 

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

365 

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

366 
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

367 
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

368 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  369 

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

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

371 

24616  372 

23388  373 
subsubsection {* List comprehension *} 
23192  374 

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

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

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

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

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

381 

382 
The qualifiers after the dot are 

383 
\begin{description} 

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

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

385 
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

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

387 
%\item[local bindings] @ {text"let x = e"}. 
24349  388 
\end{description} 
23240  389 

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

390 
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

391 
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

392 
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

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

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

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

398 
definitions for the list comprehensions in question. *} 

399 

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

400 
nonterminal lc_qual and lc_quals 
23192  401 

402 
syntax 

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

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

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

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

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

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

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

409 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  410 

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

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

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

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

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

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

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

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

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

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

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

422 
*) 
23240  423 

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

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

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

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

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

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

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

431 
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

432 
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

433 
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

434 
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

435 
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

436 

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

437 
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

438 

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

439 
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

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

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

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

443 
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

444 
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

445 
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

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

447 
Syntax.const @{syntax_const "_case1"} $ 
56241  448 
Syntax.const @{const_syntax Pure.dummy_pattern} $ NilC; 
46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

449 
val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; 
51678
1e33b81c328a
allow redundant cases in the list comprehension translation
traytel
parents:
51673
diff
changeset

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

451 

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

452 
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

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

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

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

456 
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

457 
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

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

459 
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

460 
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

461 
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

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

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

464 

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

465 
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

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

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

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

469 
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

470 
 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

471 
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

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

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

474 
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

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

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

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

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

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

480 
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

481 
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

482 
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

483 

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

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

486 

51272  487 
ML_val {* 
42167  488 
let 
489 
val read = Syntax.read_term @{context}; 

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

491 
in 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

518 
end; 

519 
*} 

520 

35115  521 
(* 
24349  522 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  523 
*) 
524 

42167  525 

50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

526 
ML {* 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

527 
(* Simproc for rewriting list comprehensions applied to List.set to set 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

528 
comprehension. *) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

529 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

530 
signature LIST_TO_SET_COMPREHENSION = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

531 
sig 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

532 
val simproc : Proof.context > cterm > thm option 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

533 
end 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

534 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

535 
structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

536 
struct 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

537 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

538 
(* conversion *) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

539 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

540 
fun all_exists_conv cv ctxt ct = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

541 
(case Thm.term_of ct of 
60156  542 
Const (@{const_name Ex}, _) $ Abs _ => 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

543 
Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

544 
 _ => cv ctxt ct) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

545 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

546 
fun all_but_last_exists_conv cv ctxt ct = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

547 
(case Thm.term_of ct of 
60156  548 
Const (@{const_name Ex}, _) $ Abs (_, _, Const (@{const_name Ex}, _) $ _) => 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

549 
Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

550 
 _ => cv ctxt ct) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

551 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

552 
fun Collect_conv cv ctxt ct = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

553 
(case Thm.term_of ct of 
60156  554 
Const (@{const_name Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

555 
 _ => raise CTERM ("Collect_conv", [ct])) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

556 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

557 
fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

558 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

559 
fun conjunct_assoc_conv ct = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

560 
Conv.try_conv 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

561 
(rewr_conv' @{thm conj_assoc} then_conv HOLogic.conj_conv Conv.all_conv conjunct_assoc_conv) ct 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

562 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

563 
fun right_hand_set_comprehension_conv conv ctxt = 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

564 
HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

565 
(Collect_conv (all_exists_conv conv o #2) ctxt)) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

566 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

567 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

568 
(* term abstraction of list comprehension patterns *) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

569 

60156  570 
datatype termlets = If  Case of typ * int 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

571 

60158  572 
local 
573 

574 
val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])} 

575 
val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} 

576 
val inst_Collect_mem_eq = @{lemma "set A = {x. x \<in> set A}" by simp} 

577 
val del_refl_eq = @{lemma "(t = t \<and> P) \<equiv> P" by simp} 

578 

579 
fun mk_set T = Const (@{const_name set}, HOLogic.listT T > HOLogic.mk_setT T) 

580 
fun dest_set (Const (@{const_name set}, _) $ xs) = xs 

581 

582 
fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name Nil}, _))) = t 

583 
 dest_singleton_list t = raise TERM ("dest_singleton_list", [t]) 

584 

585 
(*We check that one case returns a singleton list and all other cases 

586 
return [], and return the index of the one singleton list case.*) 

587 
fun possible_index_of_singleton_case cases = 

50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

588 
let 
60158  589 
fun check (i, case_t) s = 
590 
(case strip_abs_body case_t of 

591 
(Const (@{const_name Nil}, _)) => s 

592 
 _ => (case s of SOME NONE => SOME (SOME i)  _ => NONE)) 

593 
in 

594 
fold_index check cases (SOME NONE) > the_default NONE 

595 
end 

596 

597 
(*returns condition continuing term option*) 

598 
fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = 

599 
SOME (cond, then_t) 

600 
 dest_if _ = NONE 

601 

602 
(*returns (case_expr type index chosen_case constr_name) option*) 

603 
fun dest_case ctxt case_term = 

604 
let 

605 
val (case_const, args) = strip_comb case_term 

606 
in 

607 
(case try dest_Const case_const of 

608 
SOME (c, T) => 

609 
(case Ctr_Sugar.ctr_sugar_of_case ctxt c of 

610 
SOME {ctrs, ...} => 

611 
(case possible_index_of_singleton_case (fst (split_last args)) of 

612 
SOME i => 

613 
let 

614 
val constr_names = map (fst o dest_Const) ctrs 

615 
val (Ts, _) = strip_type T 

616 
val T' = List.last Ts 

617 
in SOME (List.last args, T', i, nth args i, nth constr_names i) end 

50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

618 
 NONE => NONE) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

619 
 NONE => NONE) 
60158  620 
 NONE => NONE) 
621 
end 

622 

623 
fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 

624 
 tac ctxt (If :: cont) = 

625 
Splitter.split_tac ctxt @{thms split_if} 1 

626 
THEN rtac @{thm conjI} 1 

627 
THEN rtac @{thm impI} 1 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

628 
THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => 
60158  629 
CONVERSION (right_hand_set_comprehension_conv (K 
630 
(HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv 

631 
then_conv 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

632 
rewr_conv' @{lemma "(True \<and> P) = P" by simp})) ctxt') 1) ctxt 1 
60158  633 
THEN tac ctxt cont 
634 
THEN rtac @{thm impI} 1 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

635 
THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => 
60158  636 
CONVERSION (right_hand_set_comprehension_conv (K 
637 
(HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

638 
then_conv rewr_conv' @{lemma "(False \<and> P) = False" by simp})) ctxt') 1) ctxt 1 
60158  639 
THEN rtac set_Nil_I 1 
640 
 tac ctxt (Case (T, i) :: cont) = 

641 
let 

642 
val SOME {injects, distincts, case_thms, split, ...} = 

643 
Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T)) 

644 
in 

645 
(* do case distinction *) 

646 
Splitter.split_tac ctxt [split] 1 

647 
THEN EVERY (map_index (fn (i', _) => 

648 
(if i' < length case_thms  1 then rtac @{thm conjI} 1 else all_tac) 

649 
THEN REPEAT_DETERM (rtac @{thm allI} 1) 

50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

650 
THEN rtac @{thm impI} 1 
60158  651 
THEN (if i' = i then 
652 
(* continue recursively *) 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

653 
Subgoal.FOCUS (fn {prems, context = ctxt', ...} => 
60158  654 
CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K 
655 
((HOLogic.conj_conv 

656 
(HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv 

657 
(Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects)))) 

658 
Conv.all_conv) 

659 
then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

660 
then_conv conjunct_assoc_conv)) ctxt' 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

661 
then_conv 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

662 
(HOLogic.Trueprop_conv 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

663 
(HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt'') => 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

664 
Conv.repeat_conv 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

665 
(all_but_last_exists_conv 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

666 
(K (rewr_conv' 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

667 
@{lemma "(\<exists>x. x = t \<and> P x) = P t" by simp})) ctxt'')) ctxt')))) 1) ctxt 1 
60158  668 
THEN tac ctxt cont 
669 
else 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

670 
Subgoal.FOCUS (fn {prems, context = ctxt', ...} => 
60158  671 
CONVERSION 
672 
(right_hand_set_comprehension_conv (K 

673 
(HOLogic.conj_conv 

674 
((HOLogic.eq_conv Conv.all_conv 

675 
(rewr_conv' (List.last prems))) then_conv 

676 
(Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts))) 

677 
Conv.all_conv then_conv 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

678 
(rewr_conv' @{lemma "(False \<and> P) = False" by simp}))) ctxt' then_conv 
60158  679 
HOLogic.Trueprop_conv 
680 
(HOLogic.eq_conv Conv.all_conv 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

681 
(Collect_conv (fn (_, ctxt'') => 
60158  682 
Conv.repeat_conv 
683 
(Conv.bottom_conv 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

684 
(K (rewr_conv' @{lemma "(\<exists>x. P) = P" by simp})) ctxt'')) ctxt'))) 1) ctxt 1 
60158  685 
THEN rtac set_Nil_I 1)) case_thms) 
686 
end 

687 

688 
in 

689 

690 
fun simproc ctxt redex = 

691 
let 

50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

692 
fun make_inner_eqs bound_vs Tis eqs t = 
60158  693 
(case dest_case ctxt t of 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

694 
SOME (x, T, i, cont, constr_name) => 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

695 
let 
52131  696 
val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont) 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

697 
val x' = incr_boundvars (length vs) x 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

698 
val eqs' = map (incr_boundvars (length vs)) eqs 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

699 
val constr_t = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

700 
list_comb 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

701 
(Const (constr_name, map snd vs > T), map Bound (((length vs)  1) downto 0)) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

702 
val constr_eq = Const (@{const_name HOL.eq}, T > T > @{typ bool}) $ constr_t $ x' 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

703 
in 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

704 
make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

705 
end 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

706 
 NONE => 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

707 
(case dest_if t of 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

708 
SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

709 
 NONE => 
60158  710 
if null eqs then NONE (*no rewriting, nothing to be done*) 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

711 
else 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

712 
let 
60156  713 
val Type (@{type_name list}, [rT]) = fastype_of1 (map snd bound_vs, t) 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

714 
val pat_eq = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

715 
(case try dest_singleton_list t of 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

716 
SOME t' => 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

717 
Const (@{const_name HOL.eq}, rT > rT > @{typ bool}) $ 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

718 
Bound (length bound_vs) $ t' 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

719 
 NONE => 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

720 
Const (@{const_name Set.member}, rT > HOLogic.mk_setT rT > @{typ bool}) $ 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

721 
Bound (length bound_vs) $ (mk_set rT $ t)) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

722 
val reverse_bounds = curry subst_bounds 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

723 
((map Bound ((length bound_vs  1) downto 0)) @ [Bound (length bound_vs)]) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

724 
val eqs' = map reverse_bounds eqs 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

725 
val pat_eq' = reverse_bounds pat_eq 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

726 
val inner_t = 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

727 
fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

728 
(rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq') 
59582  729 
val lhs = Thm.term_of redex 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

730 
val rhs = HOLogic.mk_Collect ("x", rT, inner_t) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

731 
val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

732 
in 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

733 
SOME 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

734 
((Goal.prove ctxt [] [] rewrite_rule_t 
60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

735 
(fn {context = ctxt', ...} => tac ctxt' (rev Tis))) RS @{thm eq_reflection}) 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

736 
end)) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

737 
in 
59582  738 
make_inner_eqs [] [] [] (dest_set (Thm.term_of redex)) 
50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

739 
end 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

740 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

741 
end 
60158  742 

743 
end 

50422
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time)  relevant for any application using it, e.g. small paper sessions;
wenzelm
parents:
50134
diff
changeset

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

745 

60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

746 
simproc_setup list_to_set_comprehension ("set xs") = 
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

747 
{* K List_to_Set_Comprehension.simproc *} 
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

748 

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

749 
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

750 
hide_const (open) coset 
35115  751 

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

752 

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

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

754 

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

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

756 
"xs \<noteq> x # xs" 
13145  757 
by (induct xs) auto 
13114  758 

58807  759 
lemma not_Cons_self2 [simp]: "x # xs \<noteq> xs" 
41697  760 
by (rule not_Cons_self [symmetric]) 
13114  761 

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

53689  765 
lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])" 
766 
by (cases xs) auto 

767 

768 
lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])" 

769 
by (cases xs) auto 

770 

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

772 
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 
53689  773 
by (fact measure_induct) 
13114  774 

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

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

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

779 
shows "P xs" 

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

781 
case Nil then show ?case by simp 

782 
next 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

783 
case (Cons x xs) 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

784 
show ?case 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

785 
proof (cases xs) 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

786 
case Nil 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

787 
with single show ?thesis by simp 
37289  788 
next 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

789 
case Cons 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

790 
show ?thesis 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

791 
proof (rule cons) 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

792 
from Cons show "xs \<noteq> []" by simp 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

793 
with Cons.hyps show "P xs" . 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

794 
qed 
37289  795 
qed 
796 
qed 

797 

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

13114  800 

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

801 

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

802 
subsubsection {* @{const length} *} 
13114  803 

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

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

806 
append_eq_append_conv}. 
13142  807 
*} 
13114  808 

13142  809 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  810 
by (induct xs) auto 
13114  811 

13142  812 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  813 
by (induct xs) auto 
13114  814 

13142  815 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  816 
by (induct xs) auto 
13114  817 

13142  818 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  819 
by (cases xs) auto 
13114  820 

13142  821 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  822 
by (induct xs) auto 
13114  823 

13142  824 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  825 
by (induct xs) auto 
13114  826 

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

829 

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

13142  833 

14025  834 
lemma Suc_length_conv: 
58807  835 
"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" 
14208  836 
apply (induct xs, simp, simp) 
14025  837 
apply blast 
838 
done 

839 

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

840 
lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False" 
58807  841 
by (induct xs) auto 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

842 

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

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

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

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

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

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

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

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

850 
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

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

852 

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

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

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

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

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

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

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

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

860 
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

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

862 
qed 
13114  863 

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

864 
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

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

866 
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

867 
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

868 
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

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

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

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

872 
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

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

874 

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

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

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

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

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

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

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

881 
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

882 

55524
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55473
diff
changeset

883 
lemma list_all2_iff: 
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55473
diff
changeset

884 
"list_all2 P xs ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)" 
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55473
diff
changeset

885 
by (induct xs ys rule: list_induct2') auto 
f41ef840f09d
folded 'list_all2' with the relator generated by 'datatype_new'
blanchet
parents:
55473
diff
changeset

886 

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

887 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  888 
by (rule Eq_FalseI) auto 
24037  889 

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

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

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

892 
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

893 
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

894 
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

895 
*) 
24037  896 

897 
let 

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

898 

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

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

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

903 
 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

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

905 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

906 
val ss = simpset_of @{context}; 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

907 

9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

908 
fun list_neq ctxt ct = 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

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

911 
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

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

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

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

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

917 
val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len); 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

918 
val thm = Goal.prove ctxt [] [] neq_len 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

919 
(K (simp_tac (put_simpset ss ctxt) 1)); 
22633  920 
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

921 
in 
23214  922 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
923 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

925 
end; 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

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

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

928 

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

929 

15392  930 
subsubsection {* @{text "@"}  append *} 
13114  931 

13142  932 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  933 
by (induct xs) auto 
13114  934 

13142  935 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  936 
by (induct xs) auto 
3507  937 

13142  938 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  939 
by (induct xs) auto 
13114  940 

13142  941 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  942 
by (induct xs) auto 
13114  943 

13142  944 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  945 
by (induct xs) auto 
13114  946 

13142  947 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  948 
by (induct xs) auto 
13114  949 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53954
diff
changeset

950 
lemma append_eq_append_conv [simp]: 
58807  951 
"length xs = length ys \<or> length us = length vs 
952 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 

24526  953 
apply (induct xs arbitrary: ys) 
14208  954 
apply (case_tac ys, simp, force) 
955 
apply (case_tac ys, force, simp) 

13145  956 
done 
13142  957 

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

960 
apply (induct xs arbitrary: ys zs ts) 

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

961 
apply fastforce 
14495  962 
apply(case_tac zs) 
963 
apply simp 

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

964 
apply fastforce 
14495  965 
done 
966 

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

967 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  968 
by simp 
13142  969 

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

13145  971 
by simp 
13114  972 

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

973 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  974 
by simp 
13114  975 

13142  976 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  977 
using append_same_eq [of _ _ "[]"] by auto 
3507  978 

13142  979 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  980 
using append_same_eq [of "[]"] by auto 
13114  981 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53954
diff
changeset

982 
lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
13145  983 
by (induct xs) auto 
13114  984 

13142  985 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  986 
by (induct xs) auto 
13114  987 

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

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

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

997 

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

1000 
by(cases ys) auto 

1001 

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

1004 
by(cases ys) auto 

1005 

14300  1006 

13142  1007 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  1008 

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

13145  1010 
by simp 
13114  1011 

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

13114  1015 

13142  1016 
lemma append_eq_appendI: 
13145  1017 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
1018 
by (drule sym) simp 

13114  1019 

1020 

13142  1021 
text {* 
13145  1022 
Simplification procedure for all list equalities. 
1023 
Currently only tries to rearrange @{text "@"} to see if 

1024 
 both lists end in a singleton list, 

1025 
 or both lists end in the same list. 

13142  1026 
*} 
1027 

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

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

1033 
 last t = t; 

1034 

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

1036 
 list1 _ = false; 

1037 

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

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

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

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

1042 

1043 
val rearr_ss = 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

1044 
simpset_of (put_simpset HOL_basic_ss @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

1045 
addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]); 
43594  1046 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

1047 
fun list_eq ctxt (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 
13462  1048 
let 
43594  1049 
val lastl = last lhs and lastr = last rhs; 
1050 
fun rearr conv = 

1051 
let 

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

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

1054 
val appT = [listT,listT] > listT 

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

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

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

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

1058 
val thm = Goal.prove ctxt [] [] eq 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51678
diff
changeset

1059 
(K (simp_tac (put_simpset rearr_ss ctxt) 1)); 
43594  1060 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
1061 
in 

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

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

1064 
else NONE 

1065 
end; 

59582  1066 
in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end; 
13114  1067 
*} 
1068 

1069 

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

1070 
subsubsection {* @{const map} *} 
13114  1071 

58807  1072 
lemma hd_map: "xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)" 
1073 
by (cases xs) simp_all 

1074 

1075 
lemma map_tl: "map f (tl xs) = tl (map f xs)" 

1076 
by (cases xs) simp_all 

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

1077 

13142  1078 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  1079 
by (induct xs) simp_all 
13114  1080 

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

13142  1084 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  1085 
by (induct xs) auto 
13114  1086 

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

1087 
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

1088 
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

1089 

35208  1090 
lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)" 
58807  1091 
by (rule ext) simp 
35208  1092 

13142  1093 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  1094 
by (induct xs) auto 
13114  1095 

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

1098 

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

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

1100 
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys" 
58807  1101 
by simp 
13114  1102 

13142  1103 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  1104 
by (cases xs) auto 
13114  1105 

13142  1106 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  1107 
by (cases xs) auto 
13114  1108 

18447  1109 
lemma map_eq_Cons_conv: 
58807  1110 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  1111 
by (cases xs) auto 
13114  1112 

18447  1113 
lemma Cons_eq_map_conv: 
58807  1114 
"(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)" 
14025  1115 
by (cases ys) auto 
1116 

18447  1117 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
1118 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

1119 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

1120 

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

18447  1123 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  1124 

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

1125 
lemma map_eq_imp_length_eq: 
35510  1126 
assumes "map f xs = map g ys" 
26734  1127 
shows "length xs = length ys" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

1128 
using assms 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

1129 
proof (induct ys arbitrary: xs) 
26734  1130 
case Nil then show ?case by simp 
1131 
next 

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

35510  1133 
from Cons xs have "map f zs = map g ys" by simp 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53017
diff
changeset

1134 
with Cons have "length zs = length ys" by blast 
26734  1135 
with xs show ?case by simp 
1136 
qed 

1137 

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

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

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

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

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

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

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

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

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

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

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

1148 

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

1149 
lemma inj_on_map_eq_map: 
58807  1150 
"inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)" 
15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

1152 

13114  1153 
lemma map_injective: 
58807  1154 
"map f xs = map f ys ==> inj f ==> xs = ys" 
24526  1155 
by (induct ys arbitrary: xs) (auto dest!:injD) 
13114  1156 

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

1159 

13114  1160 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  1161 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  1162 

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

14208  1164 
apply (unfold inj_on_def, clarify) 
13145  1165 
apply (erule_tac x = "[x]" in ballE) 
14208  1166 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  1167 
apply blast 
1168 
done 

13114  1169 

14339  1170 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  1171 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  1172 

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

1175 
apply(erule map_inj_on) 

1176 
apply(blast intro:inj_onI dest:inj_onD) 

1177 
done 

1178 

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

13114  1181 

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

1182 
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

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

1184 

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

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

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

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

1188 

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

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

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

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

1192 

55467
a5c9002bc54d
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
blanchet
parents:
55466
diff
changeset

1193 
functor map: map 
47122  1194 
by (simp_all add: id_def) 
1195 

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

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

1197 

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

1198 

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

1199 
subsubsection {* @{const rev} *} 
13114  1200 

13142  1201 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  1202 
by (induct xs) auto 
13114  1203 

13142  1204 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  1205 
by (induct xs) auto 
13114  1206 

15870  1207 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
1208 
by auto 

1209 

13142  1210 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  1211 
by (induct xs) auto 
13114  1212 

13142  1213 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  1214 
by (induct xs) auto 
13114  1215 

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

1218 

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

1220 
by (cases xs) auto 

1221 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53954
diff
changeset

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

1223 
apply (induct xs arbitrary: ys, force) 
14208  1224 
apply (case_tac ys, simp, force) 
13145  1225 
done 
13114  1226 

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

1229 

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

1232 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  1233 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
1234 
done 

13114  1235 

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

13145  1238 
by (induct xs rule: rev_induct) auto 
13114  1239 

13366  1240 
lemmas rev_cases = rev_exhaust 
1241 

57577  1242 
lemma rev_nonempty_induct [consumes 1, case_names single snoc]: 
1243 
assumes "xs \<noteq> []" 

1244 
and single: "\<And>x. P [x]" 

1245 
and snoc': "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (xs@[x])" 

1246 
shows "P xs" 

1247 
using `xs \<noteq> []` proof (induct xs rule: rev_induct) 

1248 
case (snoc x xs) then show ?case 

1249 
proof (cases xs) 

1250 
case Nil thus ?thesis by (simp add: single) 

1251 
next 

1252 
case Cons with snoc show ?thesis by (fastforce intro!: snoc') 

1253 
qed 

1254 
qed simp 

1255 

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

1258 

13114  1259 

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

1260 
subsubsection {* @{const set} *} 
13114  1261 

57816
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
57599
diff
changeset

1262 
declare list.set[code_post] "pretty output" 
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
57599
diff
changeset

1263 

13142  1264 
lemma finite_set [iff]: "finite (set xs)" 
13145  1265 
by (induct xs) auto 
13114  1266 

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

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

14099  1272 

13142  1273 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  1274 
by auto 
13114  1275 

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

1278 

13142  1279 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  1280 
by (induct xs) auto 
13114  1281 

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

1284 

13142  1285 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  1286 
by (induct xs) auto 
13114  1287 

13142  1288 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  1289 
by (induct xs) auto 
13114  1290 

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

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

1295 
by (induct j) auto 
13114  1296 

13142  1297 

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

1298 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  1299 
proof (induct xs) 
26073  1300 
case Nil thus ?case by simp 
1301 
next 

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

1303 
qed 

1304 

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

26073
