author | kleing |
Mon, 05 Nov 2007 22:51:16 +0100 | |
changeset 25299 | c3542f70b0fd |
parent 23394 | 474ff28210c0 |
child 25322 | e2eac0c30ff5 |
permissions | -rw-r--r-- |
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 |