21 by intro_classes (auto simp add: prefix_def strict_prefix_def) |
21 by intro_classes (auto simp add: prefix_def strict_prefix_def) |
22 |
22 |
23 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" |
23 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" |
24 unfolding prefix_def by blast |
24 unfolding prefix_def by blast |
25 |
25 |
26 lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C" |
26 lemma prefixE [elim?]: |
27 unfolding prefix_def by blast |
27 assumes "xs \<le> ys" |
|
28 obtains zs where "ys = xs @ zs" |
|
29 using prems unfolding prefix_def by blast |
28 |
30 |
29 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" |
31 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" |
30 unfolding strict_prefix_def prefix_def by blast |
32 unfolding strict_prefix_def prefix_def by blast |
31 |
33 |
32 lemma strict_prefixE' [elim?]: |
34 lemma strict_prefixE' [elim?]: |
33 assumes lt: "xs < ys" |
35 assumes "xs < ys" |
34 and r: "!!z zs. ys = xs @ z # zs ==> C" |
36 obtains z zs where "ys = xs @ z # zs" |
35 shows C |
37 proof - |
36 proof - |
38 from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys" |
37 from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys" |
|
38 unfolding strict_prefix_def prefix_def by blast |
39 unfolding strict_prefix_def prefix_def by blast |
39 with r show ?thesis by (auto simp add: neq_Nil_conv) |
40 with that show ?thesis by (auto simp add: neq_Nil_conv) |
40 qed |
41 qed |
41 |
42 |
42 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" |
43 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" |
43 unfolding strict_prefix_def by blast |
44 unfolding strict_prefix_def by blast |
44 |
45 |
45 lemma strict_prefixE [elim?]: |
46 lemma strict_prefixE [elim?]: |
46 "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C" |
47 fixes xs ys :: "'a list" |
47 unfolding strict_prefix_def by blast |
48 assumes "xs < ys" |
|
49 obtains "xs \<le> ys" and "xs \<noteq> ys" |
|
50 using prems unfolding strict_prefix_def by blast |
48 |
51 |
49 |
52 |
50 subsection {* Basic properties of prefixes *} |
53 subsection {* Basic properties of prefixes *} |
51 |
54 |
52 theorem Nil_prefix [iff]: "[] \<le> xs" |
55 theorem Nil_prefix [iff]: "[] \<le> xs" |
161 |
164 |
162 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
165 lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
163 unfolding parallel_def by blast |
166 unfolding parallel_def by blast |
164 |
167 |
165 lemma parallelE [elim]: |
168 lemma parallelE [elim]: |
166 "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C" |
169 assumes "xs \<parallel> ys" |
167 unfolding parallel_def by blast |
170 obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
171 using prems unfolding parallel_def by blast |
168 |
172 |
169 theorem prefix_cases: |
173 theorem prefix_cases: |
170 "(xs \<le> ys ==> C) ==> |
174 obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys" |
171 (ys < xs ==> C) ==> |
|
172 (xs \<parallel> ys ==> C) ==> C" |
|
173 unfolding parallel_def strict_prefix_def by blast |
175 unfolding parallel_def strict_prefix_def by blast |
174 |
176 |
175 theorem parallel_decomp: |
177 theorem parallel_decomp: |
176 "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" |
178 "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" |
177 proof (induct xs rule: rev_induct) |
179 proof (induct xs rule: rev_induct) |
217 |
219 |
218 definition |
220 definition |
219 postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) |
221 postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) |
220 "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)" |
222 "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)" |
221 |
223 |
222 lemma postfix_refl [simp, intro!]: "xs >>= xs" |
224 lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" |
|
225 unfolding postfix_def by blast |
|
226 |
|
227 lemma postfixE [elim?]: |
|
228 assumes "xs >>= ys" |
|
229 obtains zs where "xs = zs @ ys" |
|
230 using prems unfolding postfix_def by blast |
|
231 |
|
232 lemma postfix_refl [iff]: "xs >>= xs" |
223 by (auto simp add: postfix_def) |
233 by (auto simp add: postfix_def) |
224 lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" |
234 lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" |
225 by (auto simp add: postfix_def) |
235 by (auto simp add: postfix_def) |
226 lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys" |
236 lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys" |
227 by (auto simp add: postfix_def) |
237 by (auto simp add: postfix_def) |
228 |
238 |
229 lemma Nil_postfix [iff]: "xs >>= []" |
239 lemma Nil_postfix [iff]: "xs >>= []" |
230 by (simp add: postfix_def) |
240 by (simp add: postfix_def) |
231 lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" |
241 lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" |
232 by (auto simp add:postfix_def) |
242 by (auto simp add: postfix_def) |
233 |
243 |
234 lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" |
244 lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" |
235 by (auto simp add: postfix_def) |
245 by (auto simp add: postfix_def) |
236 lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys" |
246 lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys" |
237 by (auto simp add: postfix_def) |
247 by (auto simp add: postfix_def) |
238 |
248 |
239 lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" |
249 lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" |
240 by (auto simp add: postfix_def) |
250 by (auto simp add: postfix_def) |
241 lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" |
251 lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" |
242 by(auto simp add: postfix_def) |
252 by (auto simp add: postfix_def) |
243 |
253 |
244 lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs" |
254 lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs" |
245 by (induct zs) auto |
255 proof - |
246 lemma postfix_is_subset: "xs >>= ys \<Longrightarrow> set ys \<subseteq> set xs" |
256 assume "xs >>= ys" |
247 by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma) |
257 then obtain zs where "xs = zs @ ys" .. |
248 |
258 then show ?thesis by (induct zs) auto |
249 lemma postfix_ConsD2_lemma: "x#xs = zs @ y#ys \<Longrightarrow> xs >>= ys" |
259 qed |
250 by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) |
260 |
251 lemma postfix_ConsD2: "x#xs >>= y#ys \<Longrightarrow> xs >>= ys" |
261 lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" |
252 by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma) |
262 proof - |
253 |
263 assume "x#xs >>= y#ys" |
254 lemma postfix2prefix: "(xs >>= ys) = (rev ys <= rev xs)" |
264 then obtain zs where "x#xs = zs @ y#ys" .. |
255 apply (unfold prefix_def postfix_def, safe) |
265 then show ?thesis |
256 apply (rule_tac x = "rev zs" in exI, simp) |
266 by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) |
257 apply (rule_tac x = "rev zs" in exI) |
267 qed |
258 apply (rule rev_is_rev_conv [THEN iffD1], simp) |
268 |
259 done |
269 lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs" |
|
270 proof |
|
271 assume "xs >>= ys" |
|
272 then obtain zs where "xs = zs @ ys" .. |
|
273 then have "rev xs = rev ys @ rev zs" by simp |
|
274 then show "rev ys <= rev xs" .. |
|
275 next |
|
276 assume "rev ys <= rev xs" |
|
277 then obtain zs where "rev xs = rev ys @ zs" .. |
|
278 then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp |
|
279 then have "xs = rev zs @ ys" by simp |
|
280 then show "xs >>= ys" .. |
|
281 qed |
260 |
282 |
261 end |
283 end |