author  nipkow 
Sun, 06 May 2018 13:51:37 +0200  
changeset 68083  d730a8cfc6e0 
parent 68028  1f9f973eed2a 
child 68085  7fe53815cce9 
permissions  rwrr 
13462  1 
(* Title: HOL/List.thy 
2 
Author: Tobias Nipkow 

923  3 
*) 
4 

60758  5 
section \<open>The datatype of finite lists\<close> 
13122  6 

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

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

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

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

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

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

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

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

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

20 

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

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

22 

55406  23 
lemma [case_names Nil Cons, cases type: list]: 
61799  24 
\<comment> \<open>for backward compatibility  names of variables differ\<close> 
55406  25 
"(y = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>a list. y = a # list \<Longrightarrow> P) \<Longrightarrow> P" 
26 
by (rule list.exhaust) 

27 

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

61799  29 
\<comment> \<open>for backward compatibility  names of variables differ\<close> 
55406  30 
"P [] \<Longrightarrow> (\<And>a list. P list \<Longrightarrow> P (a # list)) \<Longrightarrow> P list" 
31 
by (rule list.induct) 

32 

60758  33 
text \<open>Compatibility:\<close> 
34 

35 
setup \<open>Sign.mandatory_path "list"\<close> 

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

36 

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

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

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

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

40 

60758  41 
setup \<open>Sign.parent_path\<close> 
55404
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55148
diff
changeset

42 

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

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

44 

34941  45 
syntax 
61799  46 
\<comment> \<open>list Enumeration\<close> 
35115  47 
"_list" :: "args => 'a list" ("[(_)]") 
34941  48 

49 
translations 

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

51 
"[x]" == "x#[]" 

52 

35115  53 

60758  54 
subsection \<open>Basic list processing functions\<close> 
15302  55 

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

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

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

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

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

50548  65 

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

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

68 

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

70 
append_Nil: "[] @ ys = ys"  

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

72 

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

74 
"rev [] = []"  

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

76 

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

78 
"filter P [] = []"  

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

34941  80 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

81 
text \<open>Special syntax for filter:\<close> 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

82 
syntax (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

83 
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<_./ _])") 
34941  84 
syntax 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

85 
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_\<leftarrow>_ ./ _])") 
34941  86 
translations 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

87 
"[x<xs . P]" \<rightleftharpoons> "CONST filter (\<lambda>x. P) xs" 
34941  88 

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

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

92 

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

94 
foldr_Nil: "foldr f [] = id"  

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

96 

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

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

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

100 

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

102 
"concat [] = []"  

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

104 

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

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

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

61799  108 
\<comment> \<open>Warning: simpset does not contain this definition, but separate 
109 
theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close> 

34941  110 

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

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

61799  114 
\<comment> \<open>Warning: simpset does not contain this definition, but separate 
115 
theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close> 

34941  116 

58135  117 
primrec (nonexhaustive) nth :: "'a list => nat => 'a" (infixl "!" 100) where 
50548  118 
nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x  Suc k \<Rightarrow> xs ! k)" 
61799  119 
\<comment> \<open>Warning: simpset does not contain this definition, but separate 
120 
theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close> 

34941  121 

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

124 
"list_update (x # xs) i v = 

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

923  126 

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

127 
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

128 

923  129 
syntax 
13366  130 
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") 
131 
"" :: "lupdbind => lupdbinds" ("_") 

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

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

134 

923  135 
translations 
35115  136 
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" 
34941  137 
"xs[i:=x]" == "CONST list_update xs i x" 
138 

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

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

142 

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

144 
"dropWhile P [] = []"  

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

146 

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

148 
"zip xs [] = []"  

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

67091  150 
(case xs of [] \<Rightarrow> []  z # zs \<Rightarrow> (z, y) # zip zs ys)" 
61799  151 
\<comment> \<open>Warning: simpset does not contain this definition, but separate 
152 
theorems for \<open>xs = []\<close> and \<open>xs = z # zs\<close>\<close> 

34941  153 

66656  154 
abbreviation map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where 
155 
"map2 f xs ys \<equiv> map (\<lambda>(x,y). f x y) (zip xs ys)" 

66655  156 

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

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

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

160 

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

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

162 

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

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

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

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

166 

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

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

170 

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

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

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

173 

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

176 

177 
hide_const (open) insert union 

178 
hide_fact (open) insert_def union_def 

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

179 

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

47122  183 

61799  184 
text \<open>In the context of multisets, \<open>count_list\<close> is equivalent to 
67091  185 
@{term "count \<circ> mset"} and it it advisable to use the latter.\<close> 
60541  186 
primrec count_list :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where 
187 
"count_list [] y = 0"  

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

59728  189 

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

192 
where "extract P xs = 

67091  193 
(case dropWhile (Not \<circ> P) xs of 
55807  194 
[] \<Rightarrow> None  
67091  195 
y#ys \<Rightarrow> Some(takeWhile (Not \<circ> P) xs, y, ys))" 
55807  196 

197 
hide_const (open) "extract" 

198 

51096  199 
primrec those :: "'a option list \<Rightarrow> 'a list option" 
200 
where 

201 
"those [] = Some []"  

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

203 
None \<Rightarrow> None 

55466  204 
 Some y \<Rightarrow> map_option (Cons y) (those xs))" 
51096  205 

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

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

209 

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

211 
"removeAll x [] = []"  

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

213 

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

215 
"distinct [] \<longleftrightarrow> True"  

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

217 

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

219 
"remdups [] = []"  

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

221 

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

222 
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

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

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

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

226 

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

229 
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

230 

60758  231 
text \<open> 
61799  232 
Function \<open>size\<close> is overloaded for all datatypes. Users may 
233 
refer to the list version as \<open>length\<close>.\<close> 

13142  234 

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

15307  237 

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

240 

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

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

244 

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

246 
"rotate n = rotate1 ^^ n" 

247 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

248 
definition nths :: "'a list => nat set => 'a list" where 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

249 
"nths xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))" 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

250 

639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

251 
primrec subseqs :: "'a list \<Rightarrow> 'a list list" where 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

252 
"subseqs [] = [[]]"  
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

253 
"subseqs (x#xs) = (let xss = subseqs xs in map (Cons x) xss @ xss)" 
50548  254 

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

256 
"n_lists 0 xs = [[]]"  

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

258 

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

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

260 

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

261 
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

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

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

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

265 

65350
b149abe619f7
added shuffle product to HOL/List
eberlm <eberlm@in.tum.de>
parents:
64966
diff
changeset

266 
function shuffle where 
b149abe619f7
added shuffle product to HOL/List
eberlm <eberlm@in.tum.de>
parents:
64966
diff
changeset

267 
"shuffle [] ys = {ys}" 
b149abe619f7
added shuffle product to HOL/List
eberlm <eberlm@in.tum.de>
parents:
64966
diff
changeset

268 
 "shuffle xs [] = {xs}" 
67399  269 
 "shuffle (x # xs) (y # ys) = (#) x ` shuffle xs (y # ys) \<union> (#) y ` shuffle (x # xs) ys" 
65350
b149abe619f7
added shuffle product to HOL/List
eberlm <eberlm@in.tum.de>
parents:
64966
diff
changeset

270 
by pat_completeness simp_all 
b149abe619f7
added shuffle product to HOL/List
eberlm <eberlm@in.tum.de>
parents:
64966
diff
changeset

271 
termination by lexicographic_order 
b149abe619f7
added shuffle product to HOL/List
eberlm <eberlm@in.tum.de>
parents:
64966
diff
changeset

272 

67170  273 
text\<open>Use only if you cannot use @{const Min} instead:\<close> 
274 
fun min_list :: "'a::ord list \<Rightarrow> 'a" where 

275 
"min_list (x # xs) = (case xs of [] \<Rightarrow> x  _ \<Rightarrow> min x (min_list xs))" 

276 

277 
text\<open>Returns first minimum:\<close> 

278 
fun arg_min_list :: "('a \<Rightarrow> ('b::linorder)) \<Rightarrow> 'a list \<Rightarrow> 'a" where 

279 
"arg_min_list f [x] = x"  

280 
"arg_min_list f (x#y#zs) = (let m = arg_min_list f (y#zs) in if f x \<le> f m then x else m)" 

281 

60758  282 
text\<open> 
26771  283 
\begin{figure}[htbp] 
284 
\fbox{ 

285 
\begin{tabular}{l} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

304 
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\ 
27381  305 
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ 
306 
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\ 

66892  307 
@{lemma "shuffle [a,b] [c,d] = {[a,b,c,d],[a,c,b,d],[a,c,d,b],[c,a,b,d],[c,a,d,b],[c,d,a,b]}" 
65350
b149abe619f7
added shuffle product to HOL/List
eberlm <eberlm@in.tum.de>
parents:
64966
diff
changeset

308 
by (simp add: insert_commute)}\\ 
27381  309 
@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\ 
310 
@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\ 

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

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

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

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

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

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

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

318 
@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\ 
35295  319 
@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\ 
57198  320 
@{lemma "List.union [2,3,4] [0::int,1,2] = [4,3,0,1,2]" by (simp add: List.insert_def List.union_def)}\\ 
47122  321 
@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\ 
322 
@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\ 

60541  323 
@{lemma "count_list [0,1,0,2::int] 0 = 2" by (simp)}\\ 
55807  324 
@{lemma "List.extract (%i::int. i>0) [0,0] = None" by(simp add: extract_def)}\\ 
325 
@{lemma "List.extract (%i::int. i>0) [0,1,0,2] = Some([0], 1, [0,2])" by(simp add: extract_def)}\\ 

27381  326 
@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\ 
27693  327 
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\ 
27381  328 
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\ 
329 
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\ 

65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

330 
@{lemma "nths [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:nths_def)}\\ 
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65350
diff
changeset

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

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

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

334 
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\ 
40077  335 
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ 
67170  336 
@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\ 
337 
@{lemma "min_list [3,1,2::int] = 2" by (simp)}\\ 

338 
@{lemma "arg_min_list (\<lambda>i. i*i) [3,1,1,2::int] = 1" by (simp)} 

26771  339 
\end{tabular}} 
340 
\caption{Characteristic examples} 

341 
\label{fig:Characteristic} 

342 
\end{figure} 

29927  343 
Figure~\ref{fig:Characteristic} shows characteristic examples 
26771  344 
that should give an intuitive understanding of the above functions. 
60758  345 
\<close> 
346 

347 
text\<open>The following simple sort functions are intended for proofs, 

348 
not for efficient implementations.\<close> 

24616  349 

66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

350 
text \<open>A sorted predicate w.r.t. a relation:\<close> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

351 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

352 
fun sorted_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

353 
"sorted_wrt P [] = True"  
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

354 
"sorted_wrt P [x] = True"  
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

355 
"sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

356 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

357 
(* FIXME: define sorted in terms of sorted_wrt *) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

358 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

359 
text \<open>A classbased sorted predicate:\<close> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66358
diff
changeset

360 

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

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

362 
begin 
67479  363 

364 
fun sorted :: "'a list \<Rightarrow> bool" where 

365 
"sorted [] = True"  

366 
"sorted [x] = True"  

367 
"sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))" 

368 

369 
lemma sorted_sorted_wrt: "sorted = sorted_wrt (\<le>)" 

370 
proof (rule ext) 

371 
fix xs show "sorted xs = sorted_wrt (\<le>) xs" 

372 
by(induction xs rule: sorted.induct) auto 

373 
qed 

24697  374 

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

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

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

379 

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

382 

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

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

386 

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

387 
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

388 
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

389 
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)" 
35608  390 

67684  391 
definition stable_sort_key :: "(('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list) \<Rightarrow> bool" where 
392 
"stable_sort_key sk = 

393 
(\<forall>f xs k. filter (\<lambda>y. f y = k) (sk f xs) = filter (\<lambda>y. f y = k) xs)" 

394 

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

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

396 

24616  397 

60758  398 
subsubsection \<open>List comprehension\<close> 
399 

400 
text\<open>Input syntax for Haskelllike list comprehension notation. 

61799  401 
Typical example: \<open>[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]\<close>, 
402 
the list of all pairs of distinct elements from \<open>xs\<close> and \<open>ys\<close>. 

403 
The syntax is as in Haskell, except that \<open>\<close> becomes a dot 

404 
(like in Isabelle's set comprehension): \<open>[e. x \<leftarrow> xs, \<dots>]\<close> rather than 

24349  405 
\verb![e x < xs, ...]!. 
406 

407 
The qualifiers after the dot are 

408 
\begin{description} 

61799  409 
\item[generators] \<open>p \<leftarrow> xs\<close>, 
410 
where \<open>p\<close> is a pattern and \<open>xs\<close> an expression of list type, or 

411 
\item[guards] \<open>b\<close>, where \<open>b\<close> is a boolean expression. 

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

412 
%\item[local bindings] @ {text"let x = e"}. 
24349  413 
\end{description} 
23240  414 

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

415 
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

416 
misunderstandings, the translation into desugared form is not reversed 
61799  417 
upon output. Note that the translation of \<open>[e. x \<leftarrow> xs]\<close> is 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

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

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

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

60758  423 
definitions for the list comprehensions in question.\<close> 
24349  424 

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

425 
nonterminal lc_qual and lc_quals 
23192  426 

427 
syntax 

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

428 
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __") 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

429 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

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

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

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

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

434 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  435 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

436 
syntax (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

437 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ < _") 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61941
diff
changeset

438 

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

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

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

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

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

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

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

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

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

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

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

450 
*) 
23240  451 

60758  452 
parse_translation \<open> 
46138
85f8d8a8c711
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46133
diff
changeset

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

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

455 
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

456 
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

457 
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

458 
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

459 

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

460 
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

461 

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

462 
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

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

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

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

466 
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

467 
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

468 
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

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

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

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

473 
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

474 

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

475 
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

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

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

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

479 
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

480 
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

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

482 
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

483 
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

484 
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

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

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

487 

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

488 
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

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

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

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

492 
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

493 
 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

494 
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

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

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

497 
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

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

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

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

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

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

503 
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

504 
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

505 
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

506 

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

507 
in [(@{syntax_const "_listcompr"}, lc_tr)] end 
60758  508 
\<close> 
509 

510 
ML_val \<open> 

42167  511 
let 
60160  512 
val read = Syntax.read_term @{context} o Syntax.implode_input; 
513 
fun check s1 s2 = 

514 
read s1 aconv read s2 orelse 

515 
error ("Check failed: " ^ 

516 
quote (Input.source_content s1) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]); 

42167  517 
in 
60160  518 
check \<open>[(x,y,z). b]\<close> \<open>if b then [(x, y, z)] else []\<close>; 
519 
check \<open>[(x,y,z). x\<leftarrow>xs]\<close> \<open>map (\<lambda>x. (x, y, z)) xs\<close>; 

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

521 
check \<open>[(x,y,z). x<a, x>b]\<close> \<open>if x < a then if b < x then [(x, y, z)] else [] else []\<close>; 

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

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

524 
check \<open>[(x,y). Cons True x \<leftarrow> xs]\<close> 

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

526 
check \<open>[(x,y,z). Cons x [] \<leftarrow> xs]\<close> 

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

528 
check \<open>[(x,y,z). x<a, x>b, x=d]\<close> 

529 
\<open>if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []\<close>; 

530 
check \<open>[(x,y,z). x<a, x>b, y\<leftarrow>ys]\<close> 

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

532 
check \<open>[(x,y,z). x<a, x\<leftarrow>xs,y>b]\<close> 

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

534 
check \<open>[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]\<close> 

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

536 
check \<open>[(x,y,z). x\<leftarrow>xs, x>b, y<a]\<close> 

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

538 
check \<open>[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]\<close> 

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

540 
check \<open>[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]\<close> 

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

542 
check \<open>[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]\<close> 

543 
\<open>concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)\<close> 

42167  544 
end; 
60758  545 
\<close> 
42167  546 

35115  547 
(* 
24349  548 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  549 
*) 
550 

42167  551 

60758  552 
ML \<open> 
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

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

554 
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

555 

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

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

558 
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

559 
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

560 

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

562 
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

563 

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

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

565 

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

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

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

569 
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

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

571 

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

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

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

575 
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

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

577 

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

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

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

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

582 

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

584 

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

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

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

588 

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

590 
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

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

592 

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

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

595 

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

597 

60158  598 
local 
599 

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

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

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

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

604 

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

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

607 

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

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

610 

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

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

613 
fun possible_index_of_singleton_case cases = 

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

614 
let 
60158  615 
fun check (i, case_t) s = 
616 
(case strip_abs_body case_t of 

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

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

619 
in 

620 
fold_index check cases (SOME NONE) > the_default NONE 

621 
end 

622 

623 
(*returns condition continuing term option*) 

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

625 
SOME (cond, then_t) 

626 
 dest_if _ = NONE 

627 

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

629 
fun dest_case ctxt case_term = 

630 
let 

631 
val (case_const, args) = strip_comb case_term 

632 
in 

633 
(case try dest_Const case_const of 

634 
SOME (c, T) => 

635 
(case Ctr_Sugar.ctr_sugar_of_case ctxt c of 

636 
SOME {ctrs, ...} => 

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

638 
SOME i => 

639 
let 

640 
val constr_names = map (fst o dest_Const) ctrs 

641 
val (Ts, _) = strip_type T 

642 
val T' = List.last Ts 

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

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

644 
 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

645 
 NONE => NONE) 
60158  646 
 NONE => NONE) 
647 
end 

648 

60752  649 
fun tac ctxt [] = 
650 
resolve_tac ctxt [set_singleton] 1 ORELSE 

651 
resolve_tac ctxt [inst_Collect_mem_eq] 1 

60158  652 
 tac ctxt (If :: cont) = 
62390  653 
Splitter.split_tac ctxt @{thms if_split} 1 
60752  654 
THEN resolve_tac ctxt @{thms conjI} 1 
655 
THEN resolve_tac ctxt @{thms impI} 1 

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

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

659 
then_conv 

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

660 
rewr_conv' @{lemma "(True \<and> P) = P" by simp})) ctxt') 1) ctxt 1 
60158  661 
THEN tac ctxt cont 
60752  662 
THEN resolve_tac ctxt @{thms impI} 1 
60159
879918f4ee0f
tuned  avoid odd rebinding of "ctxt" and "context";
wenzelm
parents:
60158
diff
changeset

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

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

666 
then_conv rewr_conv' @{lemma "(False \<and> P) = False" by simp})) ctxt') 1) ctxt 1 
60752  667 
THEN resolve_tac ctxt [set_Nil_I] 1 
60158  668 
 tac ctxt (Case (T, i) :: cont) = 
669 
let 

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

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

672 
in 

673 
(* do case distinction *) 

674 
Splitter.split_tac ctxt [split] 1 

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

60752  676 
(if i' < length case_thms  1 then resolve_tac ctxt @{thms conjI} 1 else all_tac) 
677 
THEN REPEAT_DETERM (resolve_tac ctxt @{thms allI} 1) 

678 
THEN resolve_tac ctxt @{thms impI} 1 

60158  679 
THEN (if i' = i then 
680 
(* continue recursively *) 

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

681 
Subgoal.FOCUS (fn {prems, context = ctxt', ...} => 
60158  682 
CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K 
683 
((HOLogic.conj_conv 

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

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

686 
Conv.all_conv) 

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

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

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

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

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

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

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

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

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

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

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

698 
Subgoal.FOCUS (fn {prems, context = ctxt', ...} => 
60158  699 
CONVERSION 
700 
(right_hand_set_comprehension_conv (K 

701 
(HOLogic.conj_conv 

702 
((HOLogic.eq_conv Conv.all_conv 

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

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

705 
Conv.all_conv then_conv 

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

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

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

709 
(Collect_conv (fn (_, ctxt'') => 
60158  710 
Conv.repeat_conv 
711 
(Conv.bottom_conv 

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

712 
(K (rewr_conv' @{lemma "(\<exists>x. P) = P" by simp})) ctxt'')) ctxt'))) 1) ctxt 1 
60752  713 
THEN resolve_tac ctxt [set_Nil_I] 1)) case_thms) 
60158  714 
end 
715 

716 
in 

717 

718 
fun simproc ctxt redex = 

719 
let 

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

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

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

723 
let 
52131  724 
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

725 
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

726 
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

727 
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

728 
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

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

730 
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

731 
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

732 
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

733 
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

734 
 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

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

736 
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

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

739 
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

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

742 
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

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

744 
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

745 
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

746 
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

747 
 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

748 
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

749 
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

750 
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

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

752 
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

753 
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

754 
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

755 
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

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

758 
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

759 
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

760 
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

761 
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

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

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

764 
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

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

767 
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

768 

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

769 
end 
60158  770 

771 
end 

60758  772 
\<close> 
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

773 

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

774 
simproc_setup list_to_set_comprehension ("set xs") = 
60758  775 
\<open>K List_to_Set_Comprehension.simproc\<close> 
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41372
diff
changeset

776 

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

777 
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

778 
hide_const (open) coset 
35115  779 

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

780 

60758  781 
subsubsection \<open>@{const Nil} and @{const Cons}\<close> 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

782 

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

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

784 
"xs \<noteq> x # xs" 
13145  785 
by (induct xs) auto 
13114  786 

58807  787 
lemma not_Cons_self2 [simp]: "x # xs \<noteq> xs" 
41697  788 
by (rule not_Cons_self [symmetric]) 
13114  789 

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

67091  793 
lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (\<exists>x. xs = [x])" 
53689  794 
by (cases xs) auto 
795 

67091  796 
lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (\<exists>x. xs = [x])" 
53689  797 
by (cases xs) auto 
798 

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

800 
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 
53689  801 
by (fact measure_induct) 
13114  802 

67168  803 
lemma induct_list012: 
804 
"\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs" 

805 
by induction_schema (pat_completeness, lexicographic_order) 

806 

37289  807 
lemma list_nonempty_induct [consumes 1, case_names single cons]: 
67168  808 
"\<lbrakk> xs \<noteq> []; \<And>x. P [x]; \<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)\<rbrakk> \<Longrightarrow> P xs" 
809 
by(induction xs rule: induct_list012) auto 

37289  810 

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

13114  813 

67399  814 
lemma inj_on_Cons1 [simp]: "inj_on ((#) x) A" 
61630  815 
by(simp add: inj_on_def) 
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49808
diff
changeset

816 

60758  817 
subsubsection \<open>@{const length}\<close> 
818 

819 
text \<open> 

61799  820 
Needs to come before \<open>@\<close> because of theorem \<open>append_eq_append_conv\<close>. 
60758  821 
\<close> 
13114  822 

13142  823 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  824 
by (induct xs) auto 
13114  825 

13142  826 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  827 
by (induct xs) auto 
13114  828 

13142  829 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  830 
by (induct xs) auto 
13114  831 

13142  832 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  833 
by (cases xs) auto 
13114  834 

13142  835 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  836 
by (induct xs) auto 
13114  837 

13142  838 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  839 
by (induct xs) auto 
13114  840 

67613  841 
lemma length_pos_if_in_set: "x \<in> set xs \<Longrightarrow> length xs > 0" 
23479  842 
by auto 
843 

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

13142  847 

14025  848 
lemma Suc_length_conv: 
58807  849 
"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" 
14208  850 
apply (induct xs, simp, simp) 
14025  851 
apply blast 
852 
done 

853 

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

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

856 

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

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

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

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

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

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

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

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

864 
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

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

866 

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

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

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

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

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

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

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

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

874 
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

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

876 
qed 
13114  877 

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

878 
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

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

880 
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

881 
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

882 
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

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

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

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

886 
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

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

888 

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

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

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

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

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

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

895 
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

896 

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

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

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

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

900 

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

901 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  902 
by (rule Eq_FalseI) auto 
24037  903 

60758  904 
simproc_setup list_neq ("(xs::'a list) = ys") = \<open> 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

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

906 
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

907 
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

908 
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

909 
*) 
24037  910 

911 
let 

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

912 

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

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

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

917 
 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

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

919 

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

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

921 

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

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

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

925 
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

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

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

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

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

931 
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

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

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

935 
in 
67399  936 
if m < n andalso submultiset (aconv) (ls,rs) orelse 
937 
n < m andalso submultiset (aconv) (rs,ls) 

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

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

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

940 
in K list_neq end; 
60758  941 
\<close> 
942 

943 

61799  944 
subsubsection \<open>\<open>@\<close>  append\<close> 
13114  945 

63662  946 
global_interpretation append: monoid append Nil 
947 
proof 

948 
fix xs ys zs :: "'a list" 

949 
show "(xs @ ys) @ zs = xs @ (ys @ zs)" 

950 
by (induct xs) simp_all 

951 
show "xs @ [] = xs" 

952 
by (induct xs) simp_all 

953 
qed simp 

954 

13142  955 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
63662  956 
by (fact append.assoc) 
957 

958 
lemma append_Nil2: "xs @ [] = xs" 

959 
by (fact append.right_neutral) 

3507  960 

13142  961 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  962 
by (induct xs) auto 
13114  963 

13142  964 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  965 
by (induct xs) auto 
13114  966 

13142  967 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  968 
by (induct xs) auto 
13114  969 

13142  970 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  971 
by (induct xs) auto 
13114  972 

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

973 
lemma append_eq_append_conv [simp]: 
58807  974 
"length xs = length ys \<or> length us = length vs 
975 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 

24526  976 
apply (induct xs arbitrary: ys) 
14208  977 
apply (case_tac ys, simp, force) 
978 
apply (case_tac ys, force, simp) 

13145  979 
done 
13142  980 

24526  981 
lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) = 
67091  982 
(\<exists>us. xs = zs @ us \<and> us @ ys = ts \<or> xs @ us = zs \<and> ys = us @ ts)" 
24526  983 
apply (induct xs arbitrary: ys zs ts) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44635
diff
changeset

984 
apply fastforce 
14495  985 
apply(case_tac zs) 
986 
apply simp 

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

987 
apply fastforce 
14495  988 
done 
989 

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

990 
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  991 
by simp 
13142  992 

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

13145  994 
by simp 
13114  995 

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

996 
lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  997 
by simp 
13114  998 

13142  999 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  1000 
using append_same_eq [of _ _ "[]"] by auto 
3507  1001 

13142  1002 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  1003 
using append_same_eq [of "[]"] by auto 
13114  1004 

63662  1005 
lemma hd_Cons_tl: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
1006 
by (fact list.collapse) 

13114  1007 

13142  1008 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  1009 
by (induct xs) auto 
13114  1010 

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

67091  1014 
lemma tl_append: "tl (xs @ ys) = (case xs of [] \<Rightarrow> tl ys  z#zs \<Rightarrow> zs @ ys)" 
13145  1015 
by (simp split: list.split) 
13114  1016 

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

1020 

14300  1021 
lemma Cons_eq_append_conv: "x#xs = ys@zs = 
67091  1022 
(ys = [] \<and> x#xs = zs \<or> (\<exists>ys'. x#ys' = ys \<and> xs = ys'@zs))" 
14300  1023 
by(cases ys) auto 
1024 

15281  1025 
lemma append_eq_Cons_conv: "(ys@zs = x#xs) = 
67091  1026 
(ys = [] \<and> zs = x#xs \<or> (\<exists>ys'. ys = x#ys' \<and> ys'@zs = xs))" 
15281  1027 
by(cases ys) auto 
1028 

63173  1029 
lemma longest_common_prefix: 
1030 
"\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys' 

1031 
\<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')" 

1032 
by (induct xs ys rule: list_induct2') 

1033 
(blast, blast, blast, 

1034 
metis (no_types, hide_lams) append_Cons append_Nil list.sel(1)) 

14300  1035 

61799  1036 
text \<open>Trivial rules for solving \<open>@\<close>equations automatically.\<close> 
13114  1037 

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

13145  1039 
by simp 
13114  1040 

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

13114  1044 

13142  1045 
lemma append_eq_appendI: 
13145  1046 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
1047 
by (drule sym) simp 

13114  1048 

1049 

60758  1050 
text \<open> 
13145  1051 
Simplification procedure for all list equalities. 
61799  1052 
Currently only tries to rearrange \<open>@\<close> to see if 
13145  1053 
 both lists end in a singleton list, 
1054 
 or both lists end in the same list. 

60758  1055 
\<close> 
1056 

1057 
simproc_setup list_eq ("(xs::'a list) = ys") = \<open> 

13462  1058 
let 
43594  1059 
fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) = 
1060 
(case xs of Const (@{const_name Nil}, _) => cons  _ => last xs) 

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

1062 
 last t = t; 

64963  1063 

43594  1064 
fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true 
1065 
 list1 _ = false; 

64963  1066 

43594  1067 
fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) = 
1068 
(case xs of Const (@{const_name Nil}, _) => xs  _ => cons $ butlast xs) 

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

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

64963  1071 

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

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

1074 
addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]); 
64963  1075 

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

1076 
fun list_eq ctxt (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 
13462  1077 
let 
43594  1078 
val lastl = last lhs and lastr = last rhs; 
1079 
fun rearr conv = 

1080 
let 

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

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

1083 
val appT = [listT,listT] > listT 

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

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

1086 
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

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

1088 
(K (simp_tac (put_simpset rearr_ss ctxt) 1)); 
43594  1089 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
1090 
in 

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

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

1093 
else NONE 

1094 
end; 

59582  1095 
in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end; 
60758  1096 
\<close> 
1097 

1098 

1099 
subsubsection \<open>@{const map}\<close> 

13114  1100 

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

1103 

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

1105 
by (cases xs) simp_all 

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

1106 

67091  1107 
lemma map_ext: "(\<And>x. x \<in> set xs \<longrightarrow> f x = g x) ==> map f xs = map g xs" 
13145  1108 
by (induct xs) simp_all 
13114  1109 

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

13142  1113 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  1114 
by (induct xs) auto 
13114  1115 

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

1116 
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

1117 
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

1118 

67091  1119 
lemma map_comp_map[simp]: "((map f) \<circ> (map g)) = map(f \<circ> g)" 
58807  1120 
by (rule ext) simp 
35208  1121 

13142  1122 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  1123 
by (induct xs) auto 
13114  1124 

67613  1125 
lemma map_eq_conv[simp]: "(map f xs = map g xs) = (\<forall>x \<in> set xs. f x = g x)" 
13737  1126 
by (induct xs) auto 
1127 

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

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

1129 
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys" 
58807  1130 
by simp 
13114  1131 

13142  1132 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  1133 
by (cases xs) auto 
13114  1134 

13142  1135 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  1136 
by (cases xs) auto 
13114  1137 

18447  1138 
lemma map_eq_Cons_conv: 
58807  1139 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  1140 
by (cases xs) auto 
13114  1141 

18447  1142 
lemma Cons_eq_map_conv: 
58807  1143 
"(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)" 
14025  1144 
by (cases ys) auto 
1145 

18447  1146 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
1147 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

1148 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

1149 

14111  1150 
lemma ex_map_conv: 
67091  1151 
"(\<exists>xs. ys = map f xs) = (\<forall>y \<in> set ys. \<exists>x. y = f x)" 
18447  1152 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  1153 

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

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

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

1158 
proof (induct ys arbitrary: xs) 
26734  1159 
case Nil then show ?case by simp 
1160 
next 

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

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

1163 
with Cons have "length zs = length ys" by blast 
26734  1164 
with xs show ?case by simp 
1165 
qed 

64963  1166 

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

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

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

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

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

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

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

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

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

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

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

1177 

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

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

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

1181 

13114  1182 
lemma map_injective: 
58807  1183 
"map f xs = map f ys ==> inj f ==> xs = ys" 
24526  1184 
by (induct ys arbitrary: xs) (auto dest!:injD) 
13114  1185 

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

1188 

13114  1189 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  1190 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  1191 

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

64966
d53d7ca3303e
added inj_def (redundant, analogous to surj_def, bij_def);
wenzelm
parents:
64963
diff
changeset

1193 
apply (unfold inj_def) 
d53d7ca3303e
added inj_def (redundant, analogous to surj_def, bij_def);
wenzelm
parents:
64963
diff
changeset

1194 
apply clarify 
d53d7ca3303e
added inj_def (redundant, analogous to surj_def, bij_def);
wenzelm
parents:
64963
diff
changeset

1195 
apply (erule_tac x = "[x]" in allE) 
d53d7ca3303e
added inj_def (redundant, analogous to surj_def, bij_def);
wenzelm
parents:
64963
diff
changeset

1196 
apply (erule_tac x = "[y]" in allE) 
d53d7ca3303e
added inj_def (redundant, analogous to surj_def, bij_def);
wenzelm
parents:
64963
diff
changeset

1197 
apply auto 
d53d7ca3303e
added inj_def (redundant, analogous to surj_def, bij_def);
wenzelm
parents:
64963
diff
changeset

1198 
done 
13114  1199 

14339  1200 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  1201 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  1202 

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

1205 
apply(erule map_inj_on) 

1206 
apply(blast intro:inj_onI dest:inj_onD) 

1207 
done 

1208 

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

13114  1211 

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

1212 
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

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

1214 

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

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

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

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

1218 

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

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

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

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

1222 

66853  1223 
lemma map2_map_map: "map2 h (map f xs) (map g xs) = map (\<lambda>x. h (f x) (g x)) xs" 
1224 
by (induction xs) (auto) 

1225 

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

1226 
functor map: map 
47122  1227 
by (simp_all add: id_def) 
1228 

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

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

1230 

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

1231 

60758  1232 
subsubsection \<open>@{const rev}\<close> 
13114  1233 

13142  1234 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  1235 
by (induct xs) auto 
13114  1236 

13142  1237 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  1238 
by (induct xs) auto 
13114  1239 

15870  1240 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
1241 
by auto 

1242 

13142  1243 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  1244 
by (induct xs) auto 
13114  1245 

13142  1246 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  1247 
by (induct xs) auto 
13114  1248 

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

1251 

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

1253 
by (cases xs) auto 

1254 

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

1255 
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

1256 
apply (induct xs arbitrary: ys, force) 
14208  1257 
apply (case_tac ys, simp, force) 
13145  1258 
done 
13114  1259 

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

1262 

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

1265 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  1266 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
1267 
done 

13114  1268 

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

13145  1271 
by (induct xs rule: rev_induct) auto 
13114  1272 

13366  1273 
lemmas rev_cases = rev_exhaust 
1274 

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

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

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

1279 
shows "P xs" 

60758  1280 
using \<open>xs \<noteq> []\<close> proof (induct xs rule: rev_induct) 
57577  1281 
case (snoc x xs) then show ?case 
1282 
proof (cases xs) 

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

1284 
next 

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

1286 
qed 

1287 
qed simp 

1288 

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

1291 

13114  1292 

60758  1293 
subsubsection \<open>@{const set}\<close> 
13114  1294 

67443
3abf6a722518
standardized towards newstyle formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset

1295 
declare list.set[code_post] \<comment> \<open>pretty output\<close> 
57816
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
57599
diff
changeset

1296 

13142  1297 
lemma finite_set [iff]: "finite (set xs)" 
13145
59bc43b51aa2
*** empty log message *** 