author | haftmann |
Mon, 10 Dec 2007 11:24:12 +0100 | |
changeset 25595 | 6c48275f9c76 |
parent 25564 | 4ca31a3706a4 |
child 25665 | faabc08af882 |
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 |
25595 | 9 |
imports List |
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" |
|
25564 | 66 |
by (metis append_Nil2 butlast_append butlast_snoc prefixI zs) |
67 |
(* |
|
10389 | 68 |
proof (cases zs rule: rev_cases) |
69 |
assume "zs = []" |
|
70 |
with zs have "xs = ys @ [y]" by simp |
|
23254 | 71 |
then show ?thesis .. |
10389 | 72 |
next |
73 |
fix z zs' assume "zs = zs' @ [z]" |
|
74 |
with zs have "ys = xs @ zs'" by simp |
|
23254 | 75 |
then have "xs \<le> ys" .. |
76 |
then show ?thesis .. |
|
10389 | 77 |
qed |
25564 | 78 |
*) |
10389 | 79 |
next |
80 |
assume "xs = ys @ [y] \<or> xs \<le> ys" |
|
23254 | 81 |
then show "xs \<le> ys @ [y]" |
25564 | 82 |
by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7)) |
83 |
(* |
|
10389 | 84 |
proof |
85 |
assume "xs = ys @ [y]" |
|
23254 | 86 |
then show ?thesis by simp |
10389 | 87 |
next |
88 |
assume "xs \<le> ys" |
|
89 |
then obtain zs where "ys = xs @ zs" .. |
|
23254 | 90 |
then have "ys @ [y] = xs @ (zs @ [y])" by simp |
91 |
then show ?thesis .. |
|
10389 | 92 |
qed |
25564 | 93 |
*) |
10389 | 94 |
qed |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
95 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
96 |
lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" |
10389 | 97 |
by (auto simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
98 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
99 |
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" |
10389 | 100 |
by (induct xs) simp_all |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
101 |
|
10389 | 102 |
lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" |
25564 | 103 |
by (metis append_Nil2 append_self_conv order_eq_iff prefixI) |
104 |
(* |
|
10389 | 105 |
proof - |
106 |
have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) |
|
23254 | 107 |
then show ?thesis by simp |
10389 | 108 |
qed |
25564 | 109 |
*) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
110 |
lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" |
25564 | 111 |
by (metis order_le_less_trans prefixI strict_prefixE strict_prefixI) |
112 |
(* |
|
10389 | 113 |
proof - |
114 |
assume "xs \<le> ys" |
|
115 |
then obtain us where "ys = xs @ us" .. |
|
23254 | 116 |
then have "ys @ zs = xs @ (us @ zs)" by simp |
117 |
then show ?thesis .. |
|
10389 | 118 |
qed |
25564 | 119 |
*) |
14300 | 120 |
lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs" |
17201 | 121 |
by (auto simp add: prefix_def) |
14300 | 122 |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
123 |
theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))" |
10389 | 124 |
by (cases xs) (auto simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
125 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
126 |
theorem prefix_append: |
25564 | 127 |
"(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))" |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
128 |
apply (induct zs rule: rev_induct) |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
129 |
apply force |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
130 |
apply (simp del: append_assoc add: append_assoc [symmetric]) |
25564 | 131 |
apply (metis append_eq_appendI) |
132 |
(* |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
133 |
apply simp |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
134 |
apply blast |
25564 | 135 |
*) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
136 |
done |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
137 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
138 |
lemma append_one_prefix: |
25564 | 139 |
"xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys" |
140 |
by (unfold prefix_def) |
|
141 |
(metis Cons_eq_appendI append_eq_appendI append_eq_conv_conj eq_Nil_appendI nth_drop') |
|
142 |
(* |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
143 |
apply (auto simp add: nth_append) |
10389 | 144 |
apply (case_tac zs) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
145 |
apply auto |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
146 |
done |
25564 | 147 |
*) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
148 |
theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" |
10389 | 149 |
by (auto simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
150 |
|
14300 | 151 |
lemma prefix_same_cases: |
25564 | 152 |
"(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" |
153 |
by (unfold prefix_def) (metis append_eq_append_conv2) |
|
154 |
(* |
|
17201 | 155 |
apply (erule exE)+ |
156 |
apply (simp add: append_eq_append_conv_if split: if_splits) |
|
157 |
apply (rule disjI2) |
|
158 |
apply (rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI) |
|
159 |
apply clarify |
|
160 |
apply (drule sym) |
|
161 |
apply (insert append_take_drop_id [of "length xs\<^isub>2" xs\<^isub>1]) |
|
162 |
apply simp |
|
163 |
apply (rule disjI1) |
|
164 |
apply (rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI) |
|
165 |
apply clarify |
|
166 |
apply (insert append_take_drop_id [of "length xs\<^isub>1" xs\<^isub>2]) |
|
167 |
apply simp |
|
168 |
done |
|
25564 | 169 |
*) |
170 |
lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys" |
|
171 |
by (auto simp add: prefix_def) |
|
14300 | 172 |
|
25564 | 173 |
lemma take_is_prefix: "take n xs \<le> xs" |
174 |
by (unfold prefix_def) (metis append_take_drop_id) |
|
175 |
(* |
|
25299 | 176 |
apply (rule_tac x="drop n xs" in exI) |
177 |
apply simp |
|
178 |
done |
|
25564 | 179 |
*) |
25355 | 180 |
lemma map_prefixI: |
25322 | 181 |
"xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys" |
25564 | 182 |
by (clarsimp simp: prefix_def) |
25322 | 183 |
|
25299 | 184 |
lemma prefix_length_less: |
185 |
"xs < ys \<Longrightarrow> length xs < length ys" |
|
25564 | 186 |
by (clarsimp simp: strict_prefix_def prefix_def) |
187 |
(* |
|
25299 | 188 |
apply (frule prefix_length_le) |
189 |
apply (rule ccontr, simp) |
|
190 |
apply (clarsimp simp: prefix_def) |
|
191 |
done |
|
25564 | 192 |
*) |
25299 | 193 |
lemma strict_prefix_simps [simp]: |
194 |
"xs < [] = False" |
|
195 |
"[] < (x # xs) = True" |
|
196 |
"(x # xs) < (y # ys) = (x = y \<and> xs < ys)" |
|
25564 | 197 |
by (simp_all add: strict_prefix_def cong: conj_cong) |
25299 | 198 |
|
25564 | 199 |
lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys" |
200 |
apply (induct n arbitrary: xs ys) |
|
201 |
apply (case_tac ys, simp_all)[1] |
|
202 |
apply (metis order_less_trans strict_prefixI take_is_prefix) |
|
203 |
(* |
|
25299 | 204 |
apply (case_tac xs, simp) |
205 |
apply (case_tac ys, simp_all) |
|
25564 | 206 |
*) |
207 |
done |
|
25299 | 208 |
|
25355 | 209 |
lemma not_prefix_cases: |
25299 | 210 |
assumes pfx: "\<not> ps \<le> ls" |
25356 | 211 |
obtains |
212 |
(c1) "ps \<noteq> []" and "ls = []" |
|
213 |
| (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> as \<le> xs" |
|
214 |
| (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a" |
|
25299 | 215 |
proof (cases ps) |
25564 | 216 |
case Nil thus ?thesis using pfx by simp |
25299 | 217 |
next |
218 |
case (Cons a as) |
|
25564 | 219 |
hence c: "ps = a#as" . |
25299 | 220 |
show ?thesis |
221 |
proof (cases ls) |
|
25564 | 222 |
case Nil thus ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil) |
223 |
(* |
|
25355 | 224 |
have "ps \<noteq> []" by (simp add: Nil Cons) |
225 |
from this and Nil show ?thesis by (rule c1) |
|
25564 | 226 |
*) |
25299 | 227 |
next |
228 |
case (Cons x xs) |
|
229 |
show ?thesis |
|
230 |
proof (cases "x = a") |
|
25355 | 231 |
case True |
232 |
have "\<not> as \<le> xs" using pfx c Cons True by simp |
|
233 |
with c Cons True show ?thesis by (rule c2) |
|
234 |
next |
|
235 |
case False |
|
236 |
with c Cons show ?thesis by (rule c3) |
|
25299 | 237 |
qed |
238 |
qed |
|
239 |
qed |
|
240 |
||
241 |
lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: |
|
242 |
assumes np: "\<not> ps \<le> ls" |
|
25356 | 243 |
and base: "\<And>x xs. P (x#xs) []" |
244 |
and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)" |
|
245 |
and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)" |
|
246 |
shows "P ps ls" using np |
|
25299 | 247 |
proof (induct ls arbitrary: ps) |
25355 | 248 |
case Nil then show ?case |
25299 | 249 |
by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) |
250 |
next |
|
25355 | 251 |
case (Cons y ys) |
252 |
then have npfx: "\<not> ps \<le> (y # ys)" by simp |
|
253 |
then obtain x xs where pv: "ps = x # xs" |
|
25299 | 254 |
by (rule not_prefix_cases) auto |
25564 | 255 |
show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2) |
256 |
(* |
|
25299 | 257 |
from Cons |
258 |
have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp |
|
25355 | 259 |
|
25299 | 260 |
show ?case using npfx |
261 |
by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih) |
|
25564 | 262 |
*) |
25299 | 263 |
qed |
14300 | 264 |
|
25356 | 265 |
|
10389 | 266 |
subsection {* Parallel lists *} |
267 |
||
19086 | 268 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset
|
269 |
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where |
19086 | 270 |
"(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)" |
10389 | 271 |
|
272 |
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
|
25564 | 273 |
unfolding parallel_def by blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
274 |
|
10389 | 275 |
lemma parallelE [elim]: |
25564 | 276 |
assumes "xs \<parallel> ys" |
277 |
obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
278 |
using assms unfolding parallel_def by blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
279 |
|
10389 | 280 |
theorem prefix_cases: |
25564 | 281 |
obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys" |
282 |
unfolding parallel_def strict_prefix_def by blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
283 |
|
10389 | 284 |
theorem parallel_decomp: |
285 |
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" |
|
10408 | 286 |
proof (induct xs rule: rev_induct) |
11987 | 287 |
case Nil |
23254 | 288 |
then have False by auto |
289 |
then show ?case .. |
|
10408 | 290 |
next |
11987 | 291 |
case (snoc x xs) |
292 |
show ?case |
|
10408 | 293 |
proof (rule prefix_cases) |
294 |
assume le: "xs \<le> ys" |
|
295 |
then obtain ys' where ys: "ys = xs @ ys'" .. |
|
296 |
show ?thesis |
|
297 |
proof (cases ys') |
|
25564 | 298 |
assume "ys' = []" |
299 |
thus ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys) |
|
300 |
(* |
|
301 |
with ys have "xs = ys" by simp |
|
11987 | 302 |
with snoc have "[x] \<parallel> []" by auto |
23254 | 303 |
then have False by blast |
304 |
then show ?thesis .. |
|
25564 | 305 |
*) |
10389 | 306 |
next |
10408 | 307 |
fix c cs assume ys': "ys' = c # cs" |
25564 | 308 |
thus ?thesis |
309 |
by (metis Cons_eq_appendI eq_Nil_appendI parallelE prefixI same_prefix_prefix snoc.prems ys) |
|
310 |
(* |
|
11987 | 311 |
with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) |
23254 | 312 |
then have "x \<noteq> c" by auto |
10408 | 313 |
moreover have "xs @ [x] = xs @ x # []" by simp |
314 |
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) |
|
315 |
ultimately show ?thesis by blast |
|
25564 | 316 |
*) |
10389 | 317 |
qed |
10408 | 318 |
next |
23254 | 319 |
assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) |
11987 | 320 |
with snoc have False by blast |
23254 | 321 |
then show ?thesis .. |
10408 | 322 |
next |
323 |
assume "xs \<parallel> ys" |
|
11987 | 324 |
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" |
10408 | 325 |
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" |
326 |
by blast |
|
327 |
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp |
|
328 |
with neq ys show ?thesis by blast |
|
10389 | 329 |
qed |
330 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
331 |
|
25564 | 332 |
lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d" |
333 |
by (rule parallelI) |
|
334 |
(erule parallelE, erule conjE, |
|
335 |
induct rule: not_prefix_induct, simp+)+ |
|
25299 | 336 |
|
25564 | 337 |
lemma parallel_appendI: "\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y" |
338 |
by simp (rule parallel_append) |
|
25299 | 339 |
|
25356 | 340 |
lemma parallel_commute: "(a \<parallel> b) = (b \<parallel> a)" |
25564 | 341 |
unfolding parallel_def by auto |
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
342 |
|
25356 | 343 |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
344 |
subsection {* Postfix order on lists *} |
17201 | 345 |
|
19086 | 346 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset
|
347 |
postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where |
19086 | 348 |
"(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
|
349 |
|
21305 | 350 |
lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" |
25564 | 351 |
unfolding postfix_def by blast |
21305 | 352 |
|
353 |
lemma postfixE [elim?]: |
|
25564 | 354 |
assumes "xs >>= ys" |
355 |
obtains zs where "xs = zs @ ys" |
|
356 |
using assms unfolding postfix_def by blast |
|
21305 | 357 |
|
358 |
lemma postfix_refl [iff]: "xs >>= xs" |
|
14706 | 359 |
by (auto simp add: postfix_def) |
17201 | 360 |
lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" |
14706 | 361 |
by (auto simp add: postfix_def) |
17201 | 362 |
lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys" |
14706 | 363 |
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
|
364 |
|
17201 | 365 |
lemma Nil_postfix [iff]: "xs >>= []" |
14706 | 366 |
by (simp add: postfix_def) |
17201 | 367 |
lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" |
21305 | 368 |
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
|
369 |
|
17201 | 370 |
lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" |
14706 | 371 |
by (auto simp add: postfix_def) |
17201 | 372 |
lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys" |
14706 | 373 |
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
|
374 |
|
17201 | 375 |
lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" |
14706 | 376 |
by (auto simp add: postfix_def) |
17201 | 377 |
lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" |
21305 | 378 |
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
|
379 |
|
21305 | 380 |
lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs" |
381 |
proof - |
|
382 |
assume "xs >>= ys" |
|
383 |
then obtain zs where "xs = zs @ ys" .. |
|
384 |
then show ?thesis by (induct zs) auto |
|
385 |
qed |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
386 |
|
21305 | 387 |
lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" |
388 |
proof - |
|
389 |
assume "x#xs >>= y#ys" |
|
390 |
then obtain zs where "x#xs = zs @ y#ys" .. |
|
391 |
then show ?thesis |
|
392 |
by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) |
|
393 |
qed |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
394 |
|
21305 | 395 |
lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs" |
396 |
proof |
|
397 |
assume "xs >>= ys" |
|
398 |
then obtain zs where "xs = zs @ ys" .. |
|
399 |
then have "rev xs = rev ys @ rev zs" by simp |
|
400 |
then show "rev ys <= rev xs" .. |
|
401 |
next |
|
402 |
assume "rev ys <= rev xs" |
|
403 |
then obtain zs where "rev xs = rev ys @ zs" .. |
|
404 |
then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp |
|
405 |
then have "xs = rev zs @ ys" by simp |
|
406 |
then show "xs >>= ys" .. |
|
407 |
qed |
|
17201 | 408 |
|
25564 | 409 |
lemma distinct_postfix: "distinct xs \<Longrightarrow> xs >>= ys \<Longrightarrow> distinct ys" |
410 |
by (clarsimp elim!: postfixE) |
|
25299 | 411 |
|
25564 | 412 |
lemma postfix_map: "xs >>= ys \<Longrightarrow> map f xs >>= map f ys" |
413 |
by (auto elim!: postfixE intro: postfixI) |
|
25299 | 414 |
|
25356 | 415 |
lemma postfix_drop: "as >>= drop n as" |
25564 | 416 |
unfolding postfix_def |
417 |
by (rule exI [where x = "take n as"]) simp |
|
25299 | 418 |
|
25564 | 419 |
lemma postfix_take: "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys" |
420 |
by (clarsimp elim!: postfixE) |
|
25299 | 421 |
|
25356 | 422 |
lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> x \<le> y" |
25564 | 423 |
by blast |
25299 | 424 |
|
25356 | 425 |
lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> y \<le> x" |
25564 | 426 |
by blast |
25355 | 427 |
|
428 |
lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []" |
|
25564 | 429 |
unfolding parallel_def by simp |
25355 | 430 |
|
25299 | 431 |
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" |
25564 | 432 |
unfolding parallel_def by simp |
25299 | 433 |
|
25564 | 434 |
lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" |
435 |
by auto |
|
25299 | 436 |
|
25564 | 437 |
lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs" |
438 |
by (metis Cons_prefix_Cons parallelE parallelI) |
|
439 |
(* |
|
25299 | 440 |
apply simp |
441 |
apply (rule parallelI) |
|
442 |
apply simp |
|
443 |
apply (erule parallelD1) |
|
444 |
apply simp |
|
445 |
apply (erule parallelD2) |
|
446 |
done |
|
25564 | 447 |
*) |
25299 | 448 |
lemma not_equal_is_parallel: |
449 |
assumes neq: "xs \<noteq> ys" |
|
25356 | 450 |
and len: "length xs = length ys" |
451 |
shows "xs \<parallel> ys" |
|
25299 | 452 |
using len neq |
25355 | 453 |
proof (induct rule: list_induct2) |
25356 | 454 |
case 1 |
455 |
then show ?case by simp |
|
25299 | 456 |
next |
457 |
case (2 a as b bs) |
|
25355 | 458 |
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact |
25299 | 459 |
show ?case |
460 |
proof (cases "a = b") |
|
25355 | 461 |
case True |
462 |
then have "as \<noteq> bs" using 2 by simp |
|
463 |
then show ?thesis by (rule Cons_parallelI2 [OF True ih]) |
|
25299 | 464 |
next |
465 |
case False |
|
25355 | 466 |
then show ?thesis by (rule Cons_parallelI1) |
25299 | 467 |
qed |
468 |
qed |
|
22178 | 469 |
|
25355 | 470 |
|
25356 | 471 |
subsection {* Executable code *} |
22178 | 472 |
|
473 |
lemma less_eq_code [code func]: |
|
25356 | 474 |
"([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True" |
475 |
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False" |
|
476 |
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys" |
|
22178 | 477 |
by simp_all |
478 |
||
479 |
lemma less_code [code func]: |
|
25356 | 480 |
"xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False" |
481 |
"[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True" |
|
482 |
"(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys" |
|
22178 | 483 |
unfolding strict_prefix_def by auto |
484 |
||
485 |
lemmas [code func] = postfix_to_prefix |
|
486 |
||
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
487 |
end |