author  blanchet 
Wed, 19 Feb 2014 16:32:37 +0100  
changeset 55584  a879f14b6f95 
parent 55564  e81ee43ab290 
child 55642  63beb38e9258 
permissions  rwrr 
13462  1 
(* Title: HOL/List.thy 
2 
Author: Tobias Nipkow 

923  3 
*) 
4 

13114  5 
header {* The datatype of finite lists *} 
13122  6 

15131  7 
theory List 
54555  8 
imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product 
15131  9 
begin 
923  10 

55584  11 
datatype_new (set: 'a) list (map: map rel: list_all2) = 
55405
0a155051bd9d
use new selector support to define 'the', 'hd', 'tl'
blanchet
parents:
55404
diff
changeset

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

13 
 Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) 
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55525
diff
changeset

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

15 

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

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

19 
by (rule list.exhaust) 

20 

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

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

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

24 
by (rule list.induct) 

25 

55442  26 
text {* Compatibility: *} 
27 

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

28 
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

29 

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

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

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

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

33 

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

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

35 

34941  36 
syntax 
37 
 {* list Enumeration *} 

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

40 
translations 

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

42 
"[x]" == "x#[]" 

43 

35115  44 

45 
subsection {* Basic list processing functions *} 

15302  46 

50548  47 
primrec last :: "'a list \<Rightarrow> 'a" where 
48 
"last (x # xs) = (if xs = [] then x else last xs)" 

49 

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

51 
"butlast []= []"  

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

53 

55584  54 
declare list.set[simp del, code del] 
55 

56 
lemma set_simps[simp, code, code_post]: 

57 
"set [] = {}" 

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

59 
by (simp_all add: list.set) 

60 

61 
lemma set_rec: "set xs = rec_list {} (\<lambda>x _. insert x) xs" 

62 
by (induct xs) auto 

50548  63 

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

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

66 

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

68 
append_Nil: "[] @ ys = ys"  

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

70 

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

72 
"rev [] = []"  

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

74 

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

76 
"filter P [] = []"  

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

34941  78 

79 
syntax 

80 
 {* Special syntax for filter *} 

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

83 
translations 

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

85 

86 
syntax (xsymbols) 

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

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

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

94 

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

96 
foldr_Nil: "foldr f [] = id"  

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

98 

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

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

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

102 

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

104 
"concat [] = []"  

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

106 

107 
definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where 

108 
"listsum xs = foldr plus xs 0" 

109 

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

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

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

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

115 

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

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

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

121 

50548  122 
primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where 
123 
nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x  Suc k \<Rightarrow> xs ! k)" 

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

126 

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

129 
"list_update (x # xs) i v = 

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

923  131 

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

132 
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

133 

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

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

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

139 

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

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

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

147 

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

149 
"dropWhile P [] = []"  

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

151 

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

153 
"zip xs [] = []"  

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

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

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

158 

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

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

162 

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

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

164 

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

165 
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

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

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

168 

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

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

172 

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

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

175 

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

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

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

178 

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

47122  182 

183 
hide_const (open) find 

184 

51096  185 
primrec those :: "'a option list \<Rightarrow> 'a list option" 
186 
where 

187 
"those [] = Some []"  

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

189 
None \<Rightarrow> None 

55466  190 
 Some y \<Rightarrow> map_option (Cons y) (those xs))" 
51096  191 

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

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

195 

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

197 
"removeAll x [] = []"  

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

199 

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

201 
"distinct [] \<longleftrightarrow> True"  

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

203 

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

205 
"remdups [] = []"  

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

207 

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

208 
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

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

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

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

212 

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

215 
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

216 

13142  217 
text {* 
14589  218 
Function @{text size} is overloaded for all datatypes. Users may 
13366  219 
refer to the list version as @{text length}. *} 
13142  220 

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

15307  223 

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

226 

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

227 
primrec rotate1 :: "'a list \<Rightarrow> 'a list" where 
50548  228 
"rotate1 [] = []"  
229 
"rotate1 (x # xs) = xs @ [x]" 

230 

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

232 
"rotate n = rotate1 ^^ n" 

233 

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

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

236 

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

238 
"sublists [] = [[]]"  

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

240 

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

242 
"n_lists 0 xs = [[]]"  

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

244 

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

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

246 

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

247 
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

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

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

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

251 

26771  252 
text{* 
253 
\begin{figure}[htbp] 

254 
\fbox{ 

255 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

51173  272 
@{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

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

274 
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\ 
27381  275 
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ 
276 
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

304 
\label{fig:Characteristic} 

305 
\end{figure} 

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

309 

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

312 

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

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

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

315 

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

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

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

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

319 

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

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

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

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

323 

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

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

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

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

327 

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

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

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

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

331 

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

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

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

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

335 
by simp_all 
24697  336 

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

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

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

341 

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

344 

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

345 
definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
50548  346 
"insort_insert_key f x xs = 
347 
(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

348 

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

349 
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

350 
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

351 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  352 

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

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

354 

24616  355 

23388  356 
subsubsection {* List comprehension *} 
23192  357 

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

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

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

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

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

364 

365 
The qualifiers after the dot are 

366 
\begin{description} 

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

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

368 
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

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

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

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

373 
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

374 
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

375 
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

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

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

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

381 
definitions for the list comprehensions in question. *} 

382 

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

383 
nonterminal lc_qual and lc_quals 
23192  384 

385 
syntax 

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

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

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

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

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

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

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

392 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  393 

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

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

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

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

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

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

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

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

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

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

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

405 
*) 
23240  406 

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

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

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

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

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

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

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

414 
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

415 
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

416 
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

417 
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

418 
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

419 

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

420 
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

421 

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

422 
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

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

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

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

426 
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

427 
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

428 
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

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

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

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

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

433 
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

434 

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

435 
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

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

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

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

439 
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

440 
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

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

442 
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

443 
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

444 
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

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

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

447 

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

448 
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

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

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

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

452 
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

453 
 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

454 
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

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

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

457 
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

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

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

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

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

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

463 
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

464 
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

465 
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

466 

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

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

469 

51272  470 
ML_val {* 
42167  471 
let 
472 
val read = Syntax.read_term @{context}; 

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

474 
in 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

501 
end; 

502 
*} 

503 

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

42167  508 

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

509 
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

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

511 
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

512 

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

513 
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

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

515 
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

516 
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

517 

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

518 
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

519 
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

520 

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

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

522 

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

523 
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

524 
(case Thm.term_of ct 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

525 
Const (@{const_name HOL.Ex}, _) $ Abs _ => 
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 
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

527 
 _ => 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

528 

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

530 
(case Thm.term_of ct 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

531 
Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) => 
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

532 
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

533 
 _ => 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

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

536 
(case Thm.term_of ct 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

537 
Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_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

538 
 _ => 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

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

541 

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

542 
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

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

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

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 right_hand_set_comprehension_conv conv ctxt = 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

547 
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

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

549 

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 

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

552 

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 
datatype termlets = If  Case of (typ * int) 
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

554 

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

555 
fun simproc ctxt 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

556 
let 
55584  557 
val set_Nil_I = @{thm trans} OF [@{thm set_simps(1)}, @{thm empty_def}] 
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

558 
val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} 
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 
val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} 
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 
val del_refl_eq = @{lemma "(t = t & P) == P" by simp} 
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

561 
fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T > HOLogic.mk_setT 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

562 
fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs 
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 dest_singleton_list (Const (@{const_name List.Cons}, _) 
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

564 
$ t $ (Const (@{const_name List.Nil}, _))) = 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

565 
 dest_singleton_list t = raise TERM ("dest_singleton_list", [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

566 
(* We check that one case returns a singleton list and all other cases 
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 
return [], and return the index of the one singleton list case *) 
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 
fun possible_index_of_singleton_case cases = 
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 
let 
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

570 
fun check (i, case_t) s = 
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 
(case strip_abs_body case_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

572 
(Const (@{const_name List.Nil}, _)) => s 
53412
01b804df0a30
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
traytel
parents:
53374
diff
changeset

573 
 _ => (case s of SOME NONE => SOME (SOME i)  _ => NONE)) 
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

574 
in 
53412
01b804df0a30
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
traytel
parents:
53374
diff
changeset

575 
fold_index check cases (SOME NONE) > the_default NONE 
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

576 
end 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

577 
(* returns (case_expr type index chosen_case constr_name) 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

578 
fun dest_case case_term = 
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

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

580 
val (case_const, args) = strip_comb case_term 
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

581 
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

582 
(case try dest_Const case_const 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

583 
SOME (c, T) => 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

584 
(case Ctr_Sugar.ctr_sugar_of_case ctxt c of 
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

585 
SOME {ctrs, ...} => 
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

586 
(case possible_index_of_singleton_case (fst (split_last args)) 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

587 
SOME i => 
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 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

589 
val constr_names = map (fst o dest_Const) ctrs 
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

590 
val (Ts, _) = strip_type 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

591 
val T' = List.last Ts 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

592 
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

593 
 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

594 
 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

595 
 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

596 
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

597 
(* returns condition continuing term option *) 
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

598 
fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = 
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

599 
SOME (cond, then_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

600 
 dest_if _ = 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

601 
fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 
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

602 
 tac ctxt (If :: 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

603 
Splitter.split_tac [@{thm split_if}] 1 
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

604 
THEN rtac @{thm conjI} 1 
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

605 
THEN rtac @{thm impI} 1 
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

606 
THEN Subgoal.FOCUS (fn {prems, context, ...} => 
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

607 
CONVERSION (right_hand_set_comprehension_conv (K 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

608 
(HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) 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

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

610 
rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1 
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

611 
THEN tac ctxt 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

612 
THEN rtac @{thm impI} 1 
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

613 
THEN Subgoal.FOCUS (fn {prems, context, ...} => 
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

614 
CONVERSION (right_hand_set_comprehension_conv (K 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

615 
(HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) 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

616 
then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1 
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

617 
THEN rtac set_Nil_I 1 
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 
 tac ctxt (Case (T, i) :: 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

619 
let 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

620 
val SOME {injects, distincts, case_thms, split, ...} = 
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

621 
Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type 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

622 
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

623 
(* do case distinction *) 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

624 
Splitter.split_tac [split] 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

625 
THEN EVERY (map_index (fn (i', _) => 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

626 
(if i' < length case_thms  1 then rtac @{thm conjI} 1 else all_tac) 
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

627 
THEN REPEAT_DETERM (rtac @{thm allI} 1) 
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

628 
THEN rtac @{thm impI} 1 
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

629 
THEN (if i' = i then 
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

630 
(* continue recursively *) 
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

631 
Subgoal.FOCUS (fn {prems, context, ...} => 
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

632 
CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

633 
((HOLogic.conj_conv 
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

634 
(HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

635 
(Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects)))) 
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

636 
Conv.all_conv) 
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

637 
then_conv (Conv.try_conv (Conv.rewr_conv del_refl_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

638 
then_conv conjunct_assoc_conv)) context 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

639 
then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => 
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

640 
Conv.repeat_conv 
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

641 
(all_but_last_exists_conv 
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

642 
(K (rewr_conv' 
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

643 
@{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1 
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

644 
THEN tac ctxt 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

645 
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

646 
Subgoal.FOCUS (fn {prems, context, ...} => 
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

647 
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

648 
(right_hand_set_comprehension_conv (K 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

649 
(HOLogic.conj_conv 
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

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

651 
(rewr_conv' (List.last prems))) then_conv 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

652 
(Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts))) 
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

653 
Conv.all_conv then_conv 
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

654 
(rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv 
51314
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
51272
diff
changeset

655 
HOLogic.Trueprop_conv 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

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

657 
(Collect_conv (fn (_, 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

658 
Conv.repeat_conv 
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

659 
(Conv.bottom_conv 
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

660 
(K (rewr_conv' 
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

661 
@{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

662 
THEN rtac set_Nil_I 1)) case_thms) 
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

663 
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

664 
fun make_inner_eqs bound_vs Tis eqs 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

665 
(case dest_case t of 
54404
9f0f1152c875
port list comprehension simproc to 'Ctr_Sugar' abstraction
blanchet
parents:
54295
diff
changeset

666 
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

667 
let 
52131  668 
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

669 
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

670 
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

671 
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

672 
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

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

674 
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

675 
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

676 
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

677 
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

678 
 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

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

680 
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

681 
 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

682 
if eqs = [] then NONE (* no rewriting, nothing to be done *) 
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

683 
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

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

685 
val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd 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

686 
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

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

688 
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

689 
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

690 
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

691 
 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

692 
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

693 
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

694 
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

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

696 
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

697 
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

698 
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

699 
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

700 
(rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' 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

701 
val lhs = term_of redex 
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 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

703 
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

704 
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

705 
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

706 
((Goal.prove ctxt [] [] rewrite_rule_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

707 
(fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection}) 
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 
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

709 
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

710 
make_inner_eqs [] [] [] (dest_set (term_of redex)) 
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 
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

712 

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

713 
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

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

715 

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

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

717 

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

718 
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

719 

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

720 
hide_const (open) coset 
35115  721 

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

722 

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

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

724 

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

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

726 
"xs \<noteq> x # xs" 
13145  727 
by (induct xs) auto 
13114  728 

41697  729 
lemma not_Cons_self2 [simp]: 
730 
"x # xs \<noteq> xs" 

731 
by (rule not_Cons_self [symmetric]) 

13114  732 

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

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

738 

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

740 
by (cases xs) auto 

741 

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

743 
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 
53689  744 
by (fact measure_induct) 
13114  745 

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

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

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

750 
shows "P xs" 

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

752 
case Nil then show ?case by simp 

753 
next 

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

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

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

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

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

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

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

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

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

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

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

765 
qed 
37289  766 
qed 
767 
qed 

768 

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

13114  771 

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

772 

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

773 
subsubsection {* @{const length} *} 
13114  774 

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

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

777 
append_eq_append_conv}. 
13142  778 
*} 
13114  779 

13142  780 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  781 
by (induct xs) auto 
13114  782 

13142  783 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  784 
by (induct xs) auto 
13114  785 

13142  786 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  787 
by (induct xs) auto 
13114  788 

13142  789 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  790 
by (cases xs) auto 
13114  791 

13142  792 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  793 
by (induct xs) auto 
13114  794 

13142  795 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  796 
by (induct xs) auto 
13114  797 

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

800 

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

13142  804 

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

14208  807 
apply (induct xs, simp, simp) 
14025  808 
apply blast 
809 
done 

810 

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

811 
lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

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

813 

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

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

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

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

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

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

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

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

821 
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

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

823 

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

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

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

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

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

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

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

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

831 
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

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

833 
qed 
13114  834 

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

835 
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

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

837 
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

838 
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

839 
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

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

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

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

843 
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

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

845 

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

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

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

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

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

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

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

852 
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

853 

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

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

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

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

857 

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

858 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  859 
by (rule Eq_FalseI) auto 
24037  860 

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

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

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

863 
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

864 
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

865 
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

866 
*) 
24037  867 

868 
let 

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

869 

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

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

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

874 
 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

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

876 

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

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

878 

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

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

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

882 
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

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

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

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

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

888 
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

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

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

892 
in 
23214  893 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
894 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

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

899 

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

900 

15392  901 
subsubsection {* @{text "@"}  append *} 
13114  902 

13142  903 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  904 
by (induct xs) auto 
13114  905 

13142  906 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  907 
by (induct xs) auto 
3507  908 

13142  909 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  910 
by (induct xs) auto 
13114  911 

13142  912 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  913 
by (induct xs) auto 
13114  914 

13142  915 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  916 
by (induct xs) auto 
13114  917 

13142  918 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  919 
by (induct xs) auto 
13114  920 

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

921 
lemma append_eq_append_conv [simp]: 
24526  922 
"length xs = length ys \<or> length us = length vs 
13883
0451e0fb3f22
Restructured some proofs in order to get rid of rule_format attribute.
berghofe
parents:
13863
diff
changeset

923 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  924 
apply (induct xs arbitrary: ys) 
14208  925 
apply (case_tac ys, simp, force) 
926 
apply (case_tac ys, force, simp) 

13145  927 
done 
13142  928 

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

931 
apply (induct xs arbitrary: ys zs ts) 

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

932 
apply fastforce 
14495  933 
apply(case_tac zs) 
934 
apply simp 

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

935 
apply fastforce 
14495  936 
done 
937 

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

938 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  939 
by simp 
13142  940 

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

13145  942 
by simp 
13114  943 

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

944 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  945 
by simp 
13114  946 

13142  947 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  948 
using append_same_eq [of _ _ "[]"] by auto 
3507  949 

13142  950 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  951 
using append_same_eq [of "[]"] by auto 
13114  952 

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

953 
lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
13145  954 
by (induct xs) auto 
13114  955 

13142  956 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  957 
by (induct xs) auto 
13114  958 

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

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

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

968 

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

971 
by(cases ys) auto 

972 

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

975 
by(cases ys) auto 

976 

14300  977 

13142  978 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  979 

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

13145  981 
by simp 
13114  982 

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

13114  986 

13142  987 
lemma append_eq_appendI: 
13145  988 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
989 
by (drule sym) simp 

13114  990 

991 

13142  992 
text {* 
13145  993 
Simplification procedure for all list equalities. 
994 
Currently only tries to rearrange @{text "@"} to see if 

995 
 both lists end in a singleton list, 

996 
 or both lists end in the same list. 

13142  997 
*} 
998 

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

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

1004 
 last t = t; 

1005 

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

1007 
 list1 _ = false; 

1008 

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

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

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

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

1013 

1014 
val rearr_ss = 

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

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

1016 
addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]); 
43594  1017 

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

1018 
fun list_eq ctxt (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 
13462  1019 
let 
43594  1020 
val lastl = last lhs and lastr = last rhs; 
1021 
fun rearr conv = 

1022 
let 

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

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

1025 
val appT = [listT,listT] > listT 

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

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

1028 
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

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

1030 
(K (simp_tac (put_simpset rearr_ss ctxt) 1)); 
43594  1031 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
1032 
in 

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

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

1035 
else NONE 

1036 
end; 

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

1037 
in fn _ => fn ctxt => fn ct => list_eq ctxt (term_of ct) end; 
13114  1038 
*} 
1039 

1040 

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

1041 
subsubsection {* @{const map} *} 
13114  1042 

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

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

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

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

1046 

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

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

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

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

1050 

13142  1051 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  1052 
by (induct xs) simp_all 
13114  1053 

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

13142  1057 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  1058 
by (induct xs) auto 
13114  1059 

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

1060 
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

1061 
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

1062 

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

1065 
apply(simp) 

1066 
done 

1067 

13142  1068 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  1069 
by (induct xs) auto 
13114  1070 

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

1073 

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

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

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

1076 
by simp 
13114  1077 

13142  1078 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  1079 
by (cases xs) auto 
13114  1080 

13142  1081 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  1082 
by (cases xs) auto 
13114  1083 

18447  1084 
lemma map_eq_Cons_conv: 
14025  1085 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  1086 
by (cases xs) auto 
13114  1087 

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

1091 

18447  1092 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
1093 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

1094 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

1095 

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

18447  1098 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  1099 

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

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

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

1104 
proof (induct ys arbitrary: xs) 
26734  1105 
case Nil then show ?case by simp 
1106 
next 

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

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

1109 
with Cons have "length zs = length ys" by blast 
26734  1110 
with xs show ?case by simp 
1111 
qed 

1112 

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

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

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

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

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

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

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

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

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

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

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

1123 

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

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

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

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

1127 

13114  1128 
lemma map_injective: 
24526  1129 
"map f xs = map f ys ==> inj f ==> xs = ys" 
1130 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  1131 

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

1134 

13114  1135 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  1136 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  1137 

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

14208  1139 
apply (unfold inj_on_def, clarify) 
13145  1140 
apply (erule_tac x = "[x]" in ballE) 
14208  1141 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  1142 
apply blast 
1143 
done 

13114  1144 

14339  1145 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  1146 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  1147 

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

1150 
apply(erule map_inj_on) 

1151 
apply(blast intro:inj_onI dest:inj_onD) 

1152 
done 

1153 

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

13114  1156 

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

1157 
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

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

1159 

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

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

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

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

1163 

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

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

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

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

1167 

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

1168 
functor map: map 
47122  1169 
by (simp_all add: id_def) 
1170 

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

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

1172 

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

1173 

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

1174 
subsubsection {* @{const rev} *} 
13114  1175 

13142  1176 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  1177 
by (induct xs) auto 
13114  1178 

13142  1179 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  1180 
by (induct xs) auto 
13114  1181 

15870  1182 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
1183 
by auto 

1184 

13142  1185 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  1186 
by (induct xs) auto 
13114  1187 

13142  1188 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  1189 
by (induct xs) auto 
13114  1190 

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

1193 

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

1195 
by (cases xs) auto 

1196 

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

1197 
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

1198 
apply (induct xs arbitrary: ys, force) 
14208  1199 
apply (case_tac ys, simp, force) 
13145  1200 
done 
13114  1201 

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

1204 

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

1207 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  1208 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
1209 
done 

13114  1210 

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

13145  1213 
by (induct xs rule: rev_induct) auto 
13114  1214 

13366  1215 
lemmas rev_cases = rev_exhaust 
1216 

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

1219 

13114  1220 

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

1221 
subsubsection {* @{const set} *} 
13114  1222 

13142  1223 
lemma finite_set [iff]: "finite (set xs)" 
13145  1224 
by (induct xs) auto 
13114  1225 

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

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

14099  1231 

13142  1232 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  1233 
by auto 
13114  1234 

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

1237 

13142  1238 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  1239 
by (induct xs) auto 
13114  1240 

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

1243 

13142  1244 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  1245 
by (induct xs) auto 
13114  1246 

13142  1247 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  1248 
by (induct xs) auto 
13114  1249 

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

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

1254 
by (induct j) auto 
13114  1255 

13142  1256 

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

1257 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  1258 
proof (induct xs) 
26073  1259 
case Nil thus ?case by simp 
1260 
next 

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

1262 
qed 

1263 

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

26073  1266 

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

1268 
proof (induct xs) 

1269 
case Nil thus ?case by simp 

18049  1270 
next 
1271 
case (Cons a xs) 

1272 
show ?case 

1273 
proof cases 

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

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

1276 
assume "x \<noteq> a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI) 
26073  1277 
qed 
1278 
qed 

1279 

1280 
lemma in_set_conv_decomp_first: 

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

26734  1282 
by (auto dest!: split_list_first) 
26073  1283 

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

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

1285 
proof (induct xs rule: rev_induct) 