author  blanchet 
Fri, 18 Oct 2013 10:43:20 +0200  
changeset 54147  97a8ff4e4ac9 
parent 53954  ccfd22f937be 
child 54295  45a5523d4a63 
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 
53012
cb82606b8215
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
kuncar
parents:
52435
diff
changeset

8 
imports Presburger Code_Numeral Quotient ATP Lifting_Set Lifting_Option Lifting_Product 
15131  9 
begin 
923  10 

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

923  14 

34941  15 
syntax 
16 
 {* list Enumeration *} 

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

19 
translations 

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

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

22 

35115  23 

24 
subsection {* Basic list processing functions *} 

15302  25 

50548  26 
primrec hd :: "'a list \<Rightarrow> 'a" where 
27 
"hd (x # xs) = x" 

28 

29 
primrec tl :: "'a list \<Rightarrow> 'a list" where 

30 
"tl [] = []"  

31 
"tl (x # xs) = xs" 

32 

33 
primrec last :: "'a list \<Rightarrow> 'a" where 

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

35 

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

37 
"butlast []= []"  

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

39 

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

41 
"set [] = {}"  

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

43 

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

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

46 

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

48 
"map f [] = []"  

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

50 

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

52 
append_Nil: "[] @ ys = ys"  

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

54 

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

56 
"rev [] = []"  

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

58 

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

60 
"filter P [] = []"  

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

34941  62 

63 
syntax 

64 
 {* Special syntax for filter *} 

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

67 
translations 

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

69 

70 
syntax (xsymbols) 

35115  71 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  72 
syntax (HTML output) 
35115  73 
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
34941  74 

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

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

78 

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

80 
foldr_Nil: "foldr f [] = id"  

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

82 

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

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

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

86 

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

88 
"concat [] = []"  

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

90 

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

92 
"listsum xs = foldr plus xs 0" 

93 

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

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

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

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

99 

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

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

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

105 

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

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

110 

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

113 
"list_update (x # xs) i v = 

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

923  115 

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

116 
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

117 

923  118 
syntax 
13366  119 
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") 
120 
"" :: "lupdbind => lupdbinds" ("_") 

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

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

123 

923  124 
translations 
35115  125 
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" 
34941  126 
"xs[i:=x]" == "CONST list_update xs i x" 
127 

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

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

131 

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

133 
"dropWhile P [] = []"  

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

135 

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

137 
"zip xs [] = []"  

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

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

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

142 

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

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

146 

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

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

148 

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

149 
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

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

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

152 

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

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

156 

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

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

159 

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

160 
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

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

162 

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

47122  166 

167 
hide_const (open) find 

168 

51096  169 
primrec those :: "'a option list \<Rightarrow> 'a list option" 
170 
where 

171 
"those [] = Some []"  

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

173 
None \<Rightarrow> None 

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

175 

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

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

179 

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

181 
"removeAll x [] = []"  

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

183 

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

185 
"distinct [] \<longleftrightarrow> True"  

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

187 

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

189 
"remdups [] = []"  

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

191 

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

192 
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

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

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

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

196 

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

199 
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

200 

13142  201 
text {* 
14589  202 
Function @{text size} is overloaded for all datatypes. Users may 
13366  203 
refer to the list version as @{text length}. *} 
13142  204 

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

15307  207 

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

210 

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

211 
primrec rotate1 :: "'a list \<Rightarrow> 'a list" where 
50548  212 
"rotate1 [] = []"  
213 
"rotate1 (x # xs) = xs @ [x]" 

214 

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

216 
"rotate n = rotate1 ^^ n" 

217 

218 
definition list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" where 

219 
"list_all2 P xs ys = 

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

221 

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

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

224 

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

226 
"sublists [] = [[]]"  

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

228 

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

230 
"n_lists 0 xs = [[]]"  

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

232 

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

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

234 

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

235 
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

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

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

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

239 

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

242 
\fbox{ 

243 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

262 
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\ 
27381  263 
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ 
264 
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ 

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

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

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

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

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

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

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

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

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

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

27381  278 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  279 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  280 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
281 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

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

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

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

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

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

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

292 
\label{fig:Characteristic} 

293 
\end{figure} 

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

297 

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

300 

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

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

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

303 

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

304 
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

305 
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

306 
 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

307 

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

308 
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

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

310 
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

311 

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

312 
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

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

314 
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

315 

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

316 
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

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

318 
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

319 

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

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

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

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

323 
by simp_all 
24697  324 

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

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

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

329 

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

332 

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

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

336 

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

337 
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

338 
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

339 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  340 

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

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

342 

24616  343 

23388  344 
subsubsection {* List comprehension *} 
23192  345 

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

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

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

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

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

352 

353 
The qualifiers after the dot are 

354 
\begin{description} 

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

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

356 
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

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

358 
%\item[local bindings] @ {text"let x = e"}. 
24349  359 
\end{description} 
23240  360 

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

361 
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

362 
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

363 
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

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

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

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

369 
definitions for the list comprehensions in question. *} 

370 

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

371 
nonterminal lc_qual and lc_quals 
23192  372 

373 
syntax 

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

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

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

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

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

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

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

380 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  381 

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

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

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

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

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

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

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

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

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

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

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

393 
*) 
23240  394 

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

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

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

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

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

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

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

402 
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

403 
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

404 
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

405 
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

406 
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

407 

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

408 
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

409 

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

410 
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

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

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

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

414 
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

415 
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

416 
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

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

418 
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

419 
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

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

421 
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

422 

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

423 
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

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

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

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

427 
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

428 
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

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

430 
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

431 
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

432 
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

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

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

435 

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

436 
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

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

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

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

440 
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

441 
 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

442 
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

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

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

445 
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

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

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

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

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

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

451 
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

452 
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

453 
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

454 

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

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

457 

51272  458 
ML_val {* 
42167  459 
let 
460 
val read = Syntax.read_term @{context}; 

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

462 
in 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

489 
end; 

490 
*} 

491 

35115  492 
(* 
24349  493 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  494 
*) 
495 

42167  496 

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

497 
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

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

499 
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

500 

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

501 
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

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

503 
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

504 
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

505 

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

506 
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

507 
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

508 

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

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

510 

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

511 
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

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

513 
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

514 
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

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

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

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

519 
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

520 
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

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

522 

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

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

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

525 
Const (@{const_name 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

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

527 

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

529 

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

530 
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

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

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

533 

ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
fun right_hand_set_comprehension_conv conv ctxt = 
51315
536a5603a138
provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm
parents:
51314
diff
changeset

535 
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

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

537 

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

538 

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

540 

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

542 

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

543 
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

544 
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

545 
val thy = Proof_Context.theory_of 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

546 
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

547 
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

548 
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

549 
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

550 
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

551 
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

552 
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

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

554 
 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

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

556 
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

557 
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

558 
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

559 
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

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

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

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

563 
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

564 
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

565 
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

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

567 
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

568 
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

569 
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

570 
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

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

572 
SOME (c, 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

573 
(case Datatype.info_of_case thy c 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

574 
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

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

576 
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

577 
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

578 
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

579 
val T' = List.last Ts 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
in SOME (List.last args, T', i, nth args i) 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

581 
 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

582 
 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

583 
 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

584 
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

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

586 
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

587 
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

588 
 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

589 
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

590 
 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

591 
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

592 
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

593 
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

594 
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

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

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

597 
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

598 
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

599 
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

600 
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

601 
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

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

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

604 
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

605 
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

606 
 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

607 
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

608 
val info = Datatype.the_info thy (fst (dest_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

609 
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

610 
(* do case distinction *) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
Splitter.split_tac [#split info] 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

612 
THEN EVERY (map_index (fn (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

613 
(if i' < length (#case_rewrites info)  1 then rtac @{thm conjI} 1 else all_tac) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

615 
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

616 
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

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

618 
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

619 
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

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

621 
(HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_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

622 
(Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info))))) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

624 
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

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

626 
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

627 
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

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

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

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

631 
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

632 
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

633 
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

634 
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

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

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

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

638 
(rewr_conv' (List.last prems))) 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

639 
(Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 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

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

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

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

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

645 
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

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

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

648 
@{lemma "(EX x. P) = P" 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

649 
THEN rtac set_Nil_I 1)) (#case_rewrites info)) 
ee729dbd1b7f
avoid ML_file in large theory files to improve performance of dependency 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 
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

651 
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

652 
(case dest_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

653 
SOME (x, 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

654 
let 
52131  655 
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

656 
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

657 
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

658 
val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) 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

659 
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

660 
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

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

662 
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

663 
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

664 
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

665 
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

666 
 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

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

668 
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

669 
 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

670 
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

671 
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

672 
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

673 
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

674 
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

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

676 
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

677 
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

678 
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

679 
 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

680 
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

681 
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

682 
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

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

684 
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

685 
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

686 
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

687 
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

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

689 
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

690 
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

691 
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

692 
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

693 
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

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

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

696 
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

697 
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

698 
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

699 
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

700 

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

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

703 

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

704 
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

705 

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

706 
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

707 

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

708 
hide_const (open) coset 
35115  709 

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

710 

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

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

712 

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

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

714 
"xs \<noteq> x # xs" 
13145  715 
by (induct xs) auto 
13114  716 

41697  717 
lemma not_Cons_self2 [simp]: 
718 
"x # xs \<noteq> xs" 

719 
by (rule not_Cons_self [symmetric]) 

13114  720 

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

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

726 

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

728 
by (cases xs) auto 

729 

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

731 
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 
53689  732 
by (fact measure_induct) 
13114  733 

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

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

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

738 
shows "P xs" 

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

740 
case Nil then show ?case by simp 

741 
next 

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

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

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

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

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

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

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

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

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

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

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

753 
qed 
37289  754 
qed 
755 
qed 

756 

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

13114  759 

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

760 

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

761 
subsubsection {* @{const length} *} 
13114  762 

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

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

765 
append_eq_append_conv}. 
13142  766 
*} 
13114  767 

13142  768 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  769 
by (induct xs) auto 
13114  770 

13142  771 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  772 
by (induct xs) auto 
13114  773 

13142  774 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  775 
by (induct xs) auto 
13114  776 

13142  777 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  778 
by (cases xs) auto 
13114  779 

13142  780 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  781 
by (induct xs) auto 
13114  782 

13142  783 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  784 
by (induct xs) auto 
13114  785 

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

788 

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

13142  792 

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

14208  795 
apply (induct xs, simp, simp) 
14025  796 
apply blast 
797 
done 

798 

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

799 
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

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

801 

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

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

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

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

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

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

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

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

809 
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

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

811 

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

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

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

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

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

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

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

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

819 
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

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

821 
qed 
13114  822 

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

823 
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

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

825 
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

826 
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

827 
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

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

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

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

831 
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

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

833 

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

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

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

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

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

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

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

840 
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

841 

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

842 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  843 
by (rule Eq_FalseI) auto 
24037  844 

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

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

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

847 
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

848 
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

849 
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

850 
*) 
24037  851 

852 
let 

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

853 

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

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

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

858 
 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

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

860 

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

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

862 

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

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

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

866 
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

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

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

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

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

872 
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

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

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

876 
in 
23214  877 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
878 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

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

883 

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

884 

15392  885 
subsubsection {* @{text "@"}  append *} 
13114  886 

13142  887 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  888 
by (induct xs) auto 
13114  889 

13142  890 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  891 
by (induct xs) auto 
3507  892 

13142  893 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  894 
by (induct xs) auto 
13114  895 

13142  896 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  897 
by (induct xs) auto 
13114  898 

13142  899 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  900 
by (induct xs) auto 
13114  901 

13142  902 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  903 
by (induct xs) auto 
13114  904 

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

905 
lemma append_eq_append_conv [simp]: 
24526  906 
"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

907 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  908 
apply (induct xs arbitrary: ys) 
14208  909 
apply (case_tac ys, simp, force) 
910 
apply (case_tac ys, force, simp) 

13145  911 
done 
13142  912 

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

915 
apply (induct xs arbitrary: ys zs ts) 

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

916 
apply fastforce 
14495  917 
apply(case_tac zs) 
918 
apply simp 

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

919 
apply fastforce 
14495  920 
done 
921 

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

922 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  923 
by simp 
13142  924 

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

13145  926 
by simp 
13114  927 

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

928 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  929 
by simp 
13114  930 

13142  931 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  932 
using append_same_eq [of _ _ "[]"] by auto 
3507  933 

13142  934 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  935 
using append_same_eq [of "[]"] by auto 
13114  936 

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

937 
lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
13145  938 
by (induct xs) auto 
13114  939 

13142  940 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  941 
by (induct xs) auto 
13114  942 

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

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

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

952 

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

955 
by(cases ys) auto 

956 

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

959 
by(cases ys) auto 

960 

14300  961 

13142  962 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  963 

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

13145  965 
by simp 
13114  966 

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

13114  970 

13142  971 
lemma append_eq_appendI: 
13145  972 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
973 
by (drule sym) simp 

13114  974 

975 

13142  976 
text {* 
13145  977 
Simplification procedure for all list equalities. 
978 
Currently only tries to rearrange @{text "@"} to see if 

979 
 both lists end in a singleton list, 

980 
 or both lists end in the same list. 

13142  981 
*} 
982 

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

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

988 
 last t = t; 

989 

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

991 
 list1 _ = false; 

992 

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

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

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

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

997 

998 
val rearr_ss = 

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

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

1000 
addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]); 
43594  1001 

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

1002 
fun list_eq ctxt (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 
13462  1003 
let 
43594  1004 
val lastl = last lhs and lastr = last rhs; 
1005 
fun rearr conv = 

1006 
let 

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

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

1009 
val appT = [listT,listT] > listT 

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

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

1012 
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

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

1014 
(K (simp_tac (put_simpset rearr_ss ctxt) 1)); 
43594  1015 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
1016 
in 

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

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

1019 
else NONE 

1020 
end; 

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

1021 
in fn _ => fn ctxt => fn ct => list_eq ctxt (term_of ct) end; 
13114  1022 
*} 
1023 

1024 

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

1025 
subsubsection {* @{const map} *} 
13114  1026 

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

1027 
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

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

1029 
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

1030 

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

1031 
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

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

1033 
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

1034 

13142  1035 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  1036 
by (induct xs) simp_all 
13114  1037 

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

13142  1041 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  1042 
by (induct xs) auto 
13114  1043 

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

1044 
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

1045 
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

1046 

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

1049 
apply(simp) 

1050 
done 

1051 

13142  1052 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  1053 
by (induct xs) auto 
13114  1054 

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

1057 

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

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

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

1060 
by simp 
13114  1061 

13142  1062 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  1063 
by (cases xs) auto 
13114  1064 

13142  1065 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  1066 
by (cases xs) auto 
13114  1067 

18447  1068 
lemma map_eq_Cons_conv: 
14025  1069 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  1070 
by (cases xs) auto 
13114  1071 

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

1075 

18447  1076 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
1077 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

1078 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

1079 

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

18447  1082 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  1083 

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

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

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

1088 
proof (induct ys arbitrary: xs) 
26734  1089 
case Nil then show ?case by simp 
1090 
next 

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

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

1093 
with Cons have "length zs = length ys" by blast 
26734  1094 
with xs show ?case by simp 
1095 
qed 

1096 

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

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

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

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

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

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

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

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

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

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

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

1107 

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

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

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

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

1111 

13114  1112 
lemma map_injective: 
24526  1113 
"map f xs = map f ys ==> inj f ==> xs = ys" 
1114 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  1115 

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

1118 

13114  1119 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  1120 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  1121 

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

14208  1123 
apply (unfold inj_on_def, clarify) 
13145  1124 
apply (erule_tac x = "[x]" in ballE) 
14208  1125 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  1126 
apply blast 
1127 
done 

13114  1128 

14339  1129 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  1130 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  1131 

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

1134 
apply(erule map_inj_on) 

1135 
apply(blast intro:inj_onI dest:inj_onD) 

1136 
done 

1137 

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

13114  1140 

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

1141 
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

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

1143 

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

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

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

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

1147 

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

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

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

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

1151 

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

1152 
enriched_type map: map 
47122  1153 
by (simp_all add: id_def) 
1154 

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

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

1156 

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

1157 

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

1158 
subsubsection {* @{const rev} *} 
13114  1159 

13142  1160 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  1161 
by (induct xs) auto 
13114  1162 

13142  1163 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  1164 
by (induct xs) auto 
13114  1165 

15870  1166 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
1167 
by auto 

1168 

13142  1169 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  1170 
by (induct xs) auto 
13114  1171 

13142  1172 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  1173 
by (induct xs) auto 
13114  1174 

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

1177 

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

1179 
by (cases xs) auto 

1180 

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

1181 
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

1182 
apply (induct xs arbitrary: ys, force) 
14208  1183 
apply (case_tac ys, simp, force) 
13145  1184 
done 
13114  1185 

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

1188 

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

1191 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  1192 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
1193 
done 

13114  1194 

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

13145  1197 
by (induct xs rule: rev_induct) auto 
13114  1198 

13366  1199 
lemmas rev_cases = rev_exhaust 
1200 

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

1203 

13114  1204 

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

1205 
subsubsection {* @{const set} *} 
13114  1206 

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

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

1208 

13142  1209 
lemma finite_set [iff]: "finite (set xs)" 
13145  1210 
by (induct xs) auto 
13114  1211 

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

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

14099  1217 

13142  1218 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  1219 
by auto 
13114  1220 

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

1223 

13142  1224 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  1225 
by (induct xs) auto 
13114  1226 

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

1229 

13142  1230 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  1231 
by (induct xs) auto 
13114  1232 

13142  1233 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  1234 
by (induct xs) auto 
13114  1235 

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

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

1240 
by (induct j) auto 
13114  1241 

13142  1242 

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

1243 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
18049  1244 
proof (induct xs) 
26073  1245 
case Nil thus ?case by simp 
1246 
next 

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

1248 
qed 

1249 

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

26073  1252 

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

1254 
proof (induct xs) 

1255 
case Nil thus ?case by simp 

18049  1256 
next 
1257 
case (Cons a xs) 

1258 
show ?case 

1259 
proof cases 

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

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

1262 
assume "x \<noteq> a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI) 
26073  1263 
qed 
1264 
qed 

1265 

1266 
lemma in_set_conv_decomp_first: 

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

26734  1268 
by (auto dest!: split_list_first) 
26073  1269 

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

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

1271 
proof (induct xs rule: rev_induct) 
26073  1272 
case Nil thus ?case by simp 
1273 
next 

1274 
case (snoc a xs) 

1275 
show ?case 

1276 
proof cases 

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

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

1279 
assume "x \<noteq> a" thus ?case using snoc by fastforce 
18049  1280 
qed 
1281 
qed 

1282 

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

26734  1285 
by (auto dest!: split_list_last) 
26073  1286 

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