author  blanchet 
Wed, 12 Feb 2014 08:35:56 +0100  
changeset 55406  186076d100d3 
parent 55405  0a155051bd9d 
child 55415  05f5fdb8d093 
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 

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

11 
datatype_new 'a list = 
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) 
923  14 

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

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

16 

55406  17 
thm list.exhaust[no_vars] 
18 

19 
lemma [case_names Nil Cons, cases type: list]: 

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

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

22 
by (rule list.exhaust) 

23 

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

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

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

27 
by (rule list.induct) 

28 

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

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

30 
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

31 

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

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

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

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

35 

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

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

37 

34941  38 
syntax 
39 
 {* list Enumeration *} 

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

42 
translations 

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

44 
"[x]" == "x#[]" 

45 

35115  46 

47 
subsection {* Basic list processing functions *} 

15302  48 

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

51 

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

53 
"butlast []= []"  

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

55 

56 
primrec set :: "'a list \<Rightarrow> 'a set" where 

57 
"set [] = {}"  

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

59 

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

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

62 

63 
primrec map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where 

64 
"map f [] = []"  

65 
"map f (x # xs) = f x # map f 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 

190 
 Some y \<Rightarrow> Option.map (Cons y) (those xs))" 

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 list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" where 

235 
"list_all2 P xs ys = 

236 
(length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))" 

237 

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

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

240 

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

242 
"sublists [] = [[]]"  

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

244 

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

246 
"n_lists 0 xs = [[]]"  

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

248 

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

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

250 

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

251 
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

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

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

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

255 

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

258 
\fbox{ 

259 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

278 
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\ 
27381  279 
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ 
280 
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ 

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

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

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

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

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

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

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

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

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

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

27381  294 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  295 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  296 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
297 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

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

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

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

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

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

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

308 
\label{fig:Characteristic} 

309 
\end{figure} 

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

313 

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

316 

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

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

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

319 

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

320 
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

321 
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

322 
 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

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

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

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

330 
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

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

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

334 
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

335 

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

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

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

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

339 
by simp_all 
24697  340 

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 
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where 
50548  342 
"insort_key f x [] = [x]"  
343 
"insort_key f x (y#ys) = 

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

345 

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

348 

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

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

352 

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

353 
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

354 
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

355 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  356 

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

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

358 

24616  359 

23388  360 
subsubsection {* List comprehension *} 
23192  361 

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

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

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

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

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

368 

369 
The qualifiers after the dot are 

370 
\begin{description} 

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

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

372 
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

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

374 
%\item[local bindings] @ {text"let x = e"}. 
24349  375 
\end{description} 
23240  376 

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

377 
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

378 
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

379 
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

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

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

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

385 
definitions for the list comprehensions in question. *} 

386 

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

387 
nonterminal lc_qual and lc_quals 
23192  388 

389 
syntax 

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

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

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

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

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

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

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

396 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  397 

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

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

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

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

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

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

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

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

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

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

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

409 
*) 
23240  410 

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

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

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

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

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

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

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

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

419 
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

420 
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

421 
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

422 
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

423 

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

424 
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

425 

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

426 
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

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

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

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

430 
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

431 
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

432 
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

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

434 
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

435 
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

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

437 
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

438 

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

439 
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

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

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

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

443 
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

444 
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

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

446 
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

447 
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

448 
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

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

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

451 

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

452 
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

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

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

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

456 
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

457 
 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

458 
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

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

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

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

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

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

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

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

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

467 
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

468 
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

469 
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

470 

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

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

473 

51272  474 
ML_val {* 
42167  475 
let 
476 
val read = Syntax.read_term @{context}; 

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

478 
in 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

505 
end; 

506 
*} 

507 

35115  508 
(* 
24349  509 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  510 
*) 
511 

42167  512 

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

513 
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

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

515 
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

516 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

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

519 
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

520 
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

521 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

523 
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

524 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
(* 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

526 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

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

529 
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

530 
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

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

532 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

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

535 
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

536 
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

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

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

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

541 
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

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

543 

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

544 
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

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

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

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

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

551 
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

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

553 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 

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

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

556 

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

557 
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

558 

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

559 
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

560 
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

561 
val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}] 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

563 
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

564 
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

565 
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

566 
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

567 
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

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

569 
 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

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

571 
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

572 
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

573 
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

574 
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

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

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

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

578 
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

579 
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

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

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

582 
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

583 
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

584 
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

585 
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

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

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

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

589 
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

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

591 
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

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

593 
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

594 
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

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

596 
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

597 
 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

598 
 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

599 
 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

600 
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

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

602 
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

603 
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

604 
 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

605 
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

606 
 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

607 
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

608 
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

609 
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

610 
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

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

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

613 
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

614 
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

615 
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

616 
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

617 
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

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

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

620 
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

621 
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

622 
 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

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

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

625 
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

626 
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

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

628 
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

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

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

631 
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

632 
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

633 
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

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

635 
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

636 
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

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

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

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

640 
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

641 
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

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

643 
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

644 
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

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

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

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

648 
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

649 
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

650 
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

651 
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

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

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

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

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

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

657 
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

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

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

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

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

662 
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

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

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

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

666 
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

667 
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

668 
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

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

670 
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

671 
let 
52131  672 
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

673 
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

674 
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

675 
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

676 
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

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

678 
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

679 
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

680 
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

681 
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

682 
 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

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

684 
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

685 
 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

686 
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

687 
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

688 
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

689 
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

690 
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

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

692 
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

693 
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

694 
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

695 
 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

696 
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

697 
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

698 
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

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

700 
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

701 
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

702 
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

703 
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

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

705 
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

706 
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

707 
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

708 
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

709 
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

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

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

712 
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

713 
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

714 
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

715 
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

716 

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

717 
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

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

719 

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

720 
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

721 

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

722 
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

723 

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

724 
hide_const (open) coset 
35115  725 

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

726 

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

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

728 

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

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

730 
"xs \<noteq> x # xs" 
13145  731 
by (induct xs) auto 
13114  732 

41697  733 
lemma not_Cons_self2 [simp]: 
734 
"x # xs \<noteq> xs" 

735 
by (rule not_Cons_self [symmetric]) 

13114  736 

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

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

742 

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

744 
by (cases xs) auto 

745 

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

747 
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 
53689  748 
by (fact measure_induct) 
13114  749 

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

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

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

754 
shows "P xs" 

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

756 
case Nil then show ?case by simp 

757 
next 

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

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

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

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

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

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

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

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

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

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

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

769 
qed 
37289  770 
qed 
771 
qed 

772 

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

13114  775 

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

776 

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

777 
subsubsection {* @{const length} *} 
13114  778 

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

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

781 
append_eq_append_conv}. 
13142  782 
*} 
13114  783 

13142  784 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  785 
by (induct xs) auto 
13114  786 

13142  787 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  788 
by (induct xs) auto 
13114  789 

13142  790 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  791 
by (induct xs) auto 
13114  792 

13142  793 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  794 
by (cases xs) auto 
13114  795 

13142  796 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  797 
by (induct xs) auto 
13114  798 

13142  799 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  800 
by (induct xs) auto 
13114  801 

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

804 

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

13142  808 

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

14208  811 
apply (induct xs, simp, simp) 
14025  812 
apply blast 
813 
done 

814 

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

815 
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

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

817 

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

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

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

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

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

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

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

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

825 
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

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

827 

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

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

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

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

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

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

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

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

835 
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

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

837 
qed 
13114  838 

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

839 
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

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

841 
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

842 
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

843 
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

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

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

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

847 
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

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

849 

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

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

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

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

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

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

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

856 
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

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 

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

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

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

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

1224 

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

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

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

14099  1233 

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

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

1239 

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

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

1245 

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

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

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

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

1256 
by (induct j) auto 
13114  1257 

13142  1258 

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

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

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

1264 
qed 

1265 

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

26073  1268 

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

1270 
proof (induct xs) 

1271 
case Nil thus ?case by simp 

18049  1272 
next 
1273 
case (Cons a xs) 

1274 
show ?case 

1275 
proof cases 

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

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

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

1281 

1282 
lemma in_set_conv_decomp_first: 

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

26734  1284 
by (auto dest!: split_list_first) 
26073  1285 

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

1286 
lemma split_list_last: "x \<in> set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs" 