author  kleing 
Mon, 05 Nov 2007 22:51:16 +0100  
changeset 25299  c3542f70b0fd 
parent 23394  474ff28210c0 
child 25322  e2eac0c30ff5 
permissions  rwrr 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Library/List_Prefix.thy 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

3 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

4 
*) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

5 

14706  6 
header {* List prefixes and postfixes *} 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

7 

15131  8 
theory List_Prefix 
15140  9 
imports Main 
15131  10 
begin 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

11 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

12 
subsection {* Prefix order on lists *} 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

13 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11987
diff
changeset

14 
instance list :: (type) ord .. 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

15 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

16 
defs (overloaded) 
10389  17 
prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs" 
18 
strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)" 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

19 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11987
diff
changeset

20 
instance list :: (type) order 
10389  21 
by intro_classes (auto simp add: prefix_def strict_prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

22 

10389  23 
lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" 
18730  24 
unfolding prefix_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

25 

21305  26 
lemma prefixE [elim?]: 
27 
assumes "xs \<le> ys" 

28 
obtains zs where "ys = xs @ zs" 

23394  29 
using assms unfolding prefix_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

30 

10870  31 
lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" 
18730  32 
unfolding strict_prefix_def prefix_def by blast 
10870  33 

34 
lemma strict_prefixE' [elim?]: 

21305  35 
assumes "xs < ys" 
36 
obtains z zs where "ys = xs @ z # zs" 

10870  37 
proof  
21305  38 
from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys" 
18730  39 
unfolding strict_prefix_def prefix_def by blast 
21305  40 
with that show ?thesis by (auto simp add: neq_Nil_conv) 
10870  41 
qed 
42 

10389  43 
lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" 
18730  44 
unfolding strict_prefix_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

45 

10389  46 
lemma strict_prefixE [elim?]: 
21305  47 
fixes xs ys :: "'a list" 
48 
assumes "xs < ys" 

49 
obtains "xs \<le> ys" and "xs \<noteq> ys" 

23394  50 
using assms unfolding strict_prefix_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

51 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

52 

10389  53 
subsection {* Basic properties of prefixes *} 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

54 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

55 
theorem Nil_prefix [iff]: "[] \<le> xs" 
10389  56 
by (simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

57 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

58 
theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])" 
10389  59 
by (induct xs) (simp_all add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

60 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

61 
lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)" 
10389  62 
proof 
63 
assume "xs \<le> ys @ [y]" 

64 
then obtain zs where zs: "ys @ [y] = xs @ zs" .. 

65 
show "xs = ys @ [y] \<or> xs \<le> ys" 

66 
proof (cases zs rule: rev_cases) 

67 
assume "zs = []" 

68 
with zs have "xs = ys @ [y]" by simp 

23254  69 
then show ?thesis .. 
10389  70 
next 
71 
fix z zs' assume "zs = zs' @ [z]" 

72 
with zs have "ys = xs @ zs'" by simp 

23254  73 
then have "xs \<le> ys" .. 
74 
then show ?thesis .. 

10389  75 
qed 
76 
next 

77 
assume "xs = ys @ [y] \<or> xs \<le> ys" 

23254  78 
then show "xs \<le> ys @ [y]" 
10389  79 
proof 
80 
assume "xs = ys @ [y]" 

23254  81 
then show ?thesis by simp 
10389  82 
next 
83 
assume "xs \<le> ys" 

84 
then obtain zs where "ys = xs @ zs" .. 

23254  85 
then have "ys @ [y] = xs @ (zs @ [y])" by simp 
86 
then show ?thesis .. 

10389  87 
qed 
88 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

89 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

90 
lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" 
10389  91 
by (auto simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

92 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

93 
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" 
10389  94 
by (induct xs) simp_all 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

95 

10389  96 
lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" 
97 
proof  

98 
have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) 

23254  99 
then show ?thesis by simp 
10389  100 
qed 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

101 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

102 
lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" 
10389  103 
proof  
104 
assume "xs \<le> ys" 

105 
then obtain us where "ys = xs @ us" .. 

23254  106 
then have "ys @ zs = xs @ (us @ zs)" by simp 
107 
then show ?thesis .. 

10389  108 
qed 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

109 

14300  110 
lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs" 
17201  111 
by (auto simp add: prefix_def) 
14300  112 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

113 
theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))" 
10389  114 
by (cases xs) (auto simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

115 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

116 
theorem prefix_append: 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

117 
"(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))" 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

118 
apply (induct zs rule: rev_induct) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

119 
apply force 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

120 
apply (simp del: append_assoc add: append_assoc [symmetric]) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

121 
apply simp 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

122 
apply blast 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

123 
done 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

124 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

125 
lemma append_one_prefix: 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

126 
"xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys" 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

127 
apply (unfold prefix_def) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

128 
apply (auto simp add: nth_append) 
10389  129 
apply (case_tac zs) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

130 
apply auto 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

131 
done 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

132 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

133 
theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" 
10389  134 
by (auto simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

135 

14300  136 
lemma prefix_same_cases: 
17201  137 
"(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1" 
138 
apply (simp add: prefix_def) 

139 
apply (erule exE)+ 

140 
apply (simp add: append_eq_append_conv_if split: if_splits) 

141 
apply (rule disjI2) 

142 
apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI) 

143 
apply clarify 

144 
apply (drule sym) 

145 
apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1]) 

146 
apply simp 

147 
apply (rule disjI1) 

148 
apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI) 

149 
apply clarify 

150 
apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2]) 

151 
apply simp 

152 
done 

14300  153 

154 
lemma set_mono_prefix: 

17201  155 
"xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys" 
156 
by (auto simp add: prefix_def) 

14300  157 

25299  158 
lemma take_is_prefix: 
159 
"take n xs \<le> xs" 

160 
apply (simp add: prefix_def) 

161 
apply (rule_tac x="drop n xs" in exI) 

162 
apply simp 

163 
done 

164 

165 
lemma prefix_length_less: 

166 
"xs < ys \<Longrightarrow> length xs < length ys" 

167 
apply (clarsimp simp: strict_prefix_def) 

168 
apply (frule prefix_length_le) 

169 
apply (rule ccontr, simp) 

170 
apply (clarsimp simp: prefix_def) 

171 
done 

172 

173 
lemma strict_prefix_simps [simp]: 

174 
"xs < [] = False" 

175 
"[] < (x # xs) = True" 

176 
"(x # xs) < (y # ys) = (x = y \<and> xs < ys)" 

177 
by (simp_all add: strict_prefix_def cong: conj_cong) 

178 

179 
lemma take_strict_prefix: 

180 
"xs < ys \<Longrightarrow> take n xs < ys" 

181 
apply (induct n arbitrary: xs ys) 

182 
apply (case_tac ys, simp_all)[1] 

183 
apply (case_tac xs, simp) 

184 
apply (case_tac ys, simp_all) 

185 
done 

186 

187 
lemma not_prefix_cases: 

188 
assumes pfx: "\<not> ps \<le> ls" 

189 
and c1: "\<lbrakk> ps \<noteq> []; ls = [] \<rbrakk> \<Longrightarrow> R" 

190 
and c2: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R" 

191 
and c3: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R" 

192 
shows "R" 

193 
proof (cases ps) 

194 
case Nil thus ?thesis using pfx by simp 

195 
next 

196 
case (Cons a as) 

197 

198 
hence c: "ps = a#as" . 

199 

200 
show ?thesis 

201 
proof (cases ls) 

202 
case Nil thus ?thesis 

203 
by (intro c1, simp add: Cons) 

204 
next 

205 
case (Cons x xs) 

206 
show ?thesis 

207 
proof (cases "x = a") 

208 
case True 

209 
show ?thesis 

210 
proof (intro c2) 

211 
show "\<not> as \<le> xs" using pfx c Cons True 

212 
by simp 

213 
qed 

214 
next 

215 
case False 

216 
show ?thesis by (rule c3) 

217 
qed 

218 
qed 

219 
qed 

220 

221 
lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: 

222 
assumes np: "\<not> ps \<le> ls" 

223 
and base: "\<And>x xs. P (x#xs) []" 

224 
and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)" 

225 
and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)" 

226 
shows "P ps ls" 

227 
using np 

228 
proof (induct ls arbitrary: ps) 

229 
case Nil thus ?case 

230 
by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) 

231 
next 

232 
case (Cons y ys) 

233 
hence npfx: "\<not> ps \<le> (y # ys)" by simp 

234 
then obtain x xs where pv: "ps = x # xs" 

235 
by (rule not_prefix_cases) auto 

236 

237 
from Cons 

238 
have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp 

239 

240 
show ?case using npfx 

241 
by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih) 

242 
qed 

14300  243 

10389  244 
subsection {* Parallel lists *} 
245 

19086  246 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset

247 
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where 
19086  248 
"(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)" 
10389  249 

250 
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" 

18730  251 
unfolding parallel_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

252 

10389  253 
lemma parallelE [elim]: 
21305  254 
assumes "xs \<parallel> ys" 
255 
obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs" 

23394  256 
using assms unfolding parallel_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

257 

10389  258 
theorem prefix_cases: 
21305  259 
obtains "xs \<le> ys"  "ys < xs"  "xs \<parallel> ys" 
18730  260 
unfolding parallel_def strict_prefix_def by blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

261 

10389  262 
theorem parallel_decomp: 
263 
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 

10408  264 
proof (induct xs rule: rev_induct) 
11987  265 
case Nil 
23254  266 
then have False by auto 
267 
then show ?case .. 

10408  268 
next 
11987  269 
case (snoc x xs) 
270 
show ?case 

10408  271 
proof (rule prefix_cases) 
272 
assume le: "xs \<le> ys" 

273 
then obtain ys' where ys: "ys = xs @ ys'" .. 

274 
show ?thesis 

275 
proof (cases ys') 

276 
assume "ys' = []" with ys have "xs = ys" by simp 

11987  277 
with snoc have "[x] \<parallel> []" by auto 
23254  278 
then have False by blast 
279 
then show ?thesis .. 

10389  280 
next 
10408  281 
fix c cs assume ys': "ys' = c # cs" 
11987  282 
with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) 
23254  283 
then have "x \<noteq> c" by auto 
10408  284 
moreover have "xs @ [x] = xs @ x # []" by simp 
285 
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) 

286 
ultimately show ?thesis by blast 

10389  287 
qed 
10408  288 
next 
23254  289 
assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) 
11987  290 
with snoc have False by blast 
23254  291 
then show ?thesis .. 
10408  292 
next 
293 
assume "xs \<parallel> ys" 

11987  294 
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 
10408  295 
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 
296 
by blast 

297 
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp 

298 
with neq ys show ?thesis by blast 

10389  299 
qed 
300 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

301 

25299  302 
lemma parallel_append: 
303 
"a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d" 

304 
by (rule parallelI) 

305 
(erule parallelE, erule conjE, 

306 
induct rule: not_prefix_induct, simp+)+ 

307 

308 
lemma parallel_appendI: 

309 
"\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y" 

310 
by simp (rule parallel_append) 

311 

312 
lemma parallel_commute: 

313 
"(a \<parallel> b) = (b \<parallel> a)" 

314 
unfolding parallel_def by auto 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

315 

1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

316 
subsection {* Postfix order on lists *} 
17201  317 

19086  318 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset

319 
postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where 
19086  320 
"(xs >>= ys) = (\<exists>zs. xs = zs @ ys)" 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

321 

21305  322 
lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" 
323 
unfolding postfix_def by blast 

324 

325 
lemma postfixE [elim?]: 

326 
assumes "xs >>= ys" 

327 
obtains zs where "xs = zs @ ys" 

23394  328 
using assms unfolding postfix_def by blast 
21305  329 

330 
lemma postfix_refl [iff]: "xs >>= xs" 

14706  331 
by (auto simp add: postfix_def) 
17201  332 
lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" 
14706  333 
by (auto simp add: postfix_def) 
17201  334 
lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys" 
14706  335 
by (auto simp add: postfix_def) 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

336 

17201  337 
lemma Nil_postfix [iff]: "xs >>= []" 
14706  338 
by (simp add: postfix_def) 
17201  339 
lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" 
21305  340 
by (auto simp add: postfix_def) 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

341 

17201  342 
lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" 
14706  343 
by (auto simp add: postfix_def) 
17201  344 
lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys" 
14706  345 
by (auto simp add: postfix_def) 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

346 

17201  347 
lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" 
14706  348 
by (auto simp add: postfix_def) 
17201  349 
lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" 
21305  350 
by (auto simp add: postfix_def) 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

351 

21305  352 
lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs" 
353 
proof  

354 
assume "xs >>= ys" 

355 
then obtain zs where "xs = zs @ ys" .. 

356 
then show ?thesis by (induct zs) auto 

357 
qed 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

358 

21305  359 
lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" 
360 
proof  

361 
assume "x#xs >>= y#ys" 

362 
then obtain zs where "x#xs = zs @ y#ys" .. 

363 
then show ?thesis 

364 
by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) 

365 
qed 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

366 

21305  367 
lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs" 
368 
proof 

369 
assume "xs >>= ys" 

370 
then obtain zs where "xs = zs @ ys" .. 

371 
then have "rev xs = rev ys @ rev zs" by simp 

372 
then show "rev ys <= rev xs" .. 

373 
next 

374 
assume "rev ys <= rev xs" 

375 
then obtain zs where "rev xs = rev ys @ zs" .. 

376 
then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp 

377 
then have "xs = rev zs @ ys" by simp 

378 
then show "xs >>= ys" .. 

379 
qed 

17201  380 

25299  381 
lemma distinct_postfix: 
382 
assumes dx: "distinct xs" 

383 
and pf: "xs >>= ys" 

384 
shows "distinct ys" 

385 
using dx pf by (clarsimp elim!: postfixE) 

386 

387 
lemma postfix_map: 

388 
assumes pf: "xs >>= ys" 

389 
shows "map f xs >>= map f ys" 

390 
using pf by (auto elim!: postfixE intro: postfixI) 

391 

392 
lemma postfix_drop: 

393 
"as >>= drop n as" 

394 
unfolding postfix_def 

395 
by (rule exI [where x = "take n as"]) simp 

396 

397 
lemma postfix_take: 

398 
"xs >>= ys \<Longrightarrow> xs = take (length xs  length ys) xs @ ys" 

399 
by (clarsimp elim!: postfixE) 

400 

401 
lemma parallelD1: 

402 
"x \<parallel> y \<Longrightarrow> \<not> x \<le> y" by blast 

403 

404 
lemma parallelD2: 

405 
"x \<parallel> y \<Longrightarrow> \<not> y \<le> x" by blast 

406 

407 
lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []" 

408 
unfolding parallel_def by simp 

409 

410 
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" 

411 
unfolding parallel_def by simp 

412 

413 
lemma Cons_parallelI1: 

414 
"a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" by auto 

415 

416 
lemma Cons_parallelI2: 

417 
"\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs" 

418 
apply simp 

419 
apply (rule parallelI) 

420 
apply simp 

421 
apply (erule parallelD1) 

422 
apply simp 

423 
apply (erule parallelD2) 

424 
done 

425 

426 
lemma not_equal_is_parallel: 

427 
assumes neq: "xs \<noteq> ys" 

428 
and len: "length xs = length ys" 

429 
shows "xs \<parallel> ys" 

430 
using len neq 

431 
proof (induct rule: list_induct2) 

432 
case 1 thus ?case by simp 

433 
next 

434 
case (2 a as b bs) 

435 

436 
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" . 

437 

438 
show ?case 

439 
proof (cases "a = b") 

440 
case True 

441 
hence "as \<noteq> bs" using 2 by simp 

442 

443 
thus ?thesis by (rule Cons_parallelI2 [OF True ih]) 

444 
next 

445 
case False 

446 
thus ?thesis by (rule Cons_parallelI1) 

447 
qed 

448 
qed 

22178  449 

450 
subsection {* Exeuctable code *} 

451 

452 
lemma less_eq_code [code func]: 

453 
"([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True" 

454 
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False" 

455 
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys" 

456 
by simp_all 

457 

458 
lemma less_code [code func]: 

459 
"xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False" 

460 
"[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True" 

461 
"(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys" 

462 
unfolding strict_prefix_def by auto 

463 

464 
lemmas [code func] = postfix_to_prefix 

465 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

466 
end 