author | wenzelm |
Thu, 08 Nov 2007 20:09:17 +0100 | |
changeset 25355 | 69c0a39ba028 |
parent 25322 | e2eac0c30ff5 |
child 25356 | 059c03630d6e |
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 |
||
25355 | 165 |
lemma map_prefixI: |
25322 | 166 |
"xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys" |
167 |
by (clarsimp simp: prefix_def) |
|
168 |
||
25299 | 169 |
lemma prefix_length_less: |
170 |
"xs < ys \<Longrightarrow> length xs < length ys" |
|
171 |
apply (clarsimp simp: strict_prefix_def) |
|
172 |
apply (frule prefix_length_le) |
|
173 |
apply (rule ccontr, simp) |
|
174 |
apply (clarsimp simp: prefix_def) |
|
175 |
done |
|
176 |
||
177 |
lemma strict_prefix_simps [simp]: |
|
178 |
"xs < [] = False" |
|
179 |
"[] < (x # xs) = True" |
|
180 |
"(x # xs) < (y # ys) = (x = y \<and> xs < ys)" |
|
181 |
by (simp_all add: strict_prefix_def cong: conj_cong) |
|
182 |
||
183 |
lemma take_strict_prefix: |
|
184 |
"xs < ys \<Longrightarrow> take n xs < ys" |
|
185 |
apply (induct n arbitrary: xs ys) |
|
186 |
apply (case_tac ys, simp_all)[1] |
|
187 |
apply (case_tac xs, simp) |
|
188 |
apply (case_tac ys, simp_all) |
|
189 |
done |
|
190 |
||
25355 | 191 |
lemma not_prefix_cases: |
25299 | 192 |
assumes pfx: "\<not> ps \<le> ls" |
193 |
and c1: "\<lbrakk> ps \<noteq> []; ls = [] \<rbrakk> \<Longrightarrow> R" |
|
194 |
and c2: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R" |
|
195 |
and c3: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R" |
|
25355 | 196 |
shows "R" |
25299 | 197 |
proof (cases ps) |
25355 | 198 |
case Nil then show ?thesis using pfx by simp |
25299 | 199 |
next |
200 |
case (Cons a as) |
|
25355 | 201 |
then have c: "ps = a#as" . |
202 |
||
25299 | 203 |
show ?thesis |
204 |
proof (cases ls) |
|
25355 | 205 |
case Nil |
206 |
have "ps \<noteq> []" by (simp add: Nil Cons) |
|
207 |
from this and Nil show ?thesis by (rule c1) |
|
25299 | 208 |
next |
209 |
case (Cons x xs) |
|
210 |
show ?thesis |
|
211 |
proof (cases "x = a") |
|
25355 | 212 |
case True |
213 |
have "\<not> as \<le> xs" using pfx c Cons True by simp |
|
214 |
with c Cons True show ?thesis by (rule c2) |
|
215 |
next |
|
216 |
case False |
|
217 |
with c Cons show ?thesis by (rule c3) |
|
25299 | 218 |
qed |
219 |
qed |
|
220 |
qed |
|
221 |
||
222 |
lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: |
|
223 |
assumes np: "\<not> ps \<le> ls" |
|
224 |
and base: "\<And>x xs. P (x#xs) []" |
|
225 |
and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)" |
|
226 |
and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)" |
|
227 |
shows "P ps ls" |
|
228 |
using np |
|
229 |
proof (induct ls arbitrary: ps) |
|
25355 | 230 |
case Nil then show ?case |
25299 | 231 |
by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) |
232 |
next |
|
25355 | 233 |
case (Cons y ys) |
234 |
then have npfx: "\<not> ps \<le> (y # ys)" by simp |
|
235 |
then obtain x xs where pv: "ps = x # xs" |
|
25299 | 236 |
by (rule not_prefix_cases) auto |
237 |
||
238 |
from Cons |
|
239 |
have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp |
|
25355 | 240 |
|
25299 | 241 |
show ?case using npfx |
242 |
by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih) |
|
243 |
qed |
|
14300 | 244 |
|
10389 | 245 |
subsection {* Parallel lists *} |
246 |
||
19086 | 247 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset
|
248 |
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where |
19086 | 249 |
"(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)" |
10389 | 250 |
|
251 |
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
|
18730 | 252 |
unfolding parallel_def by blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
253 |
|
10389 | 254 |
lemma parallelE [elim]: |
21305 | 255 |
assumes "xs \<parallel> ys" |
256 |
obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
23394 | 257 |
using assms unfolding parallel_def by blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
258 |
|
10389 | 259 |
theorem prefix_cases: |
21305 | 260 |
obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys" |
18730 | 261 |
unfolding parallel_def strict_prefix_def by blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
262 |
|
10389 | 263 |
theorem parallel_decomp: |
264 |
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" |
|
10408 | 265 |
proof (induct xs rule: rev_induct) |
11987 | 266 |
case Nil |
23254 | 267 |
then have False by auto |
268 |
then show ?case .. |
|
10408 | 269 |
next |
11987 | 270 |
case (snoc x xs) |
271 |
show ?case |
|
10408 | 272 |
proof (rule prefix_cases) |
273 |
assume le: "xs \<le> ys" |
|
274 |
then obtain ys' where ys: "ys = xs @ ys'" .. |
|
275 |
show ?thesis |
|
276 |
proof (cases ys') |
|
277 |
assume "ys' = []" with ys have "xs = ys" by simp |
|
11987 | 278 |
with snoc have "[x] \<parallel> []" by auto |
23254 | 279 |
then have False by blast |
280 |
then show ?thesis .. |
|
10389 | 281 |
next |
10408 | 282 |
fix c cs assume ys': "ys' = c # cs" |
11987 | 283 |
with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) |
23254 | 284 |
then have "x \<noteq> c" by auto |
10408 | 285 |
moreover have "xs @ [x] = xs @ x # []" by simp |
286 |
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) |
|
287 |
ultimately show ?thesis by blast |
|
10389 | 288 |
qed |
10408 | 289 |
next |
23254 | 290 |
assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) |
11987 | 291 |
with snoc have False by blast |
23254 | 292 |
then show ?thesis .. |
10408 | 293 |
next |
294 |
assume "xs \<parallel> ys" |
|
11987 | 295 |
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" |
10408 | 296 |
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" |
297 |
by blast |
|
298 |
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp |
|
299 |
with neq ys show ?thesis by blast |
|
10389 | 300 |
qed |
301 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
302 |
|
25299 | 303 |
lemma parallel_append: |
304 |
"a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d" |
|
25355 | 305 |
by (rule parallelI) |
306 |
(erule parallelE, erule conjE, |
|
25299 | 307 |
induct rule: not_prefix_induct, simp+)+ |
308 |
||
25355 | 309 |
lemma parallel_appendI: |
25299 | 310 |
"\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y" |
311 |
by simp (rule parallel_append) |
|
312 |
||
313 |
lemma parallel_commute: |
|
25355 | 314 |
"(a \<parallel> b) = (b \<parallel> a)" |
25299 | 315 |
unfolding parallel_def by auto |
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
316 |
|
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
317 |
subsection {* Postfix order on lists *} |
17201 | 318 |
|
19086 | 319 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset
|
320 |
postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where |
19086 | 321 |
"(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
|
322 |
|
21305 | 323 |
lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" |
324 |
unfolding postfix_def by blast |
|
325 |
||
326 |
lemma postfixE [elim?]: |
|
327 |
assumes "xs >>= ys" |
|
328 |
obtains zs where "xs = zs @ ys" |
|
23394 | 329 |
using assms unfolding postfix_def by blast |
21305 | 330 |
|
331 |
lemma postfix_refl [iff]: "xs >>= xs" |
|
14706 | 332 |
by (auto simp add: postfix_def) |
17201 | 333 |
lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" |
14706 | 334 |
by (auto simp add: postfix_def) |
17201 | 335 |
lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys" |
14706 | 336 |
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
|
337 |
|
17201 | 338 |
lemma Nil_postfix [iff]: "xs >>= []" |
14706 | 339 |
by (simp add: postfix_def) |
17201 | 340 |
lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" |
21305 | 341 |
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
|
342 |
|
17201 | 343 |
lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" |
14706 | 344 |
by (auto simp add: postfix_def) |
17201 | 345 |
lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys" |
14706 | 346 |
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
|
347 |
|
17201 | 348 |
lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" |
14706 | 349 |
by (auto simp add: postfix_def) |
17201 | 350 |
lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" |
21305 | 351 |
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
|
352 |
|
21305 | 353 |
lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs" |
354 |
proof - |
|
355 |
assume "xs >>= ys" |
|
356 |
then obtain zs where "xs = zs @ ys" .. |
|
357 |
then show ?thesis by (induct zs) auto |
|
358 |
qed |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
359 |
|
21305 | 360 |
lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" |
361 |
proof - |
|
362 |
assume "x#xs >>= y#ys" |
|
363 |
then obtain zs where "x#xs = zs @ y#ys" .. |
|
364 |
then show ?thesis |
|
365 |
by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) |
|
366 |
qed |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
367 |
|
21305 | 368 |
lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs" |
369 |
proof |
|
370 |
assume "xs >>= ys" |
|
371 |
then obtain zs where "xs = zs @ ys" .. |
|
372 |
then have "rev xs = rev ys @ rev zs" by simp |
|
373 |
then show "rev ys <= rev xs" .. |
|
374 |
next |
|
375 |
assume "rev ys <= rev xs" |
|
376 |
then obtain zs where "rev xs = rev ys @ zs" .. |
|
377 |
then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp |
|
378 |
then have "xs = rev zs @ ys" by simp |
|
379 |
then show "xs >>= ys" .. |
|
380 |
qed |
|
17201 | 381 |
|
25299 | 382 |
lemma distinct_postfix: |
383 |
assumes dx: "distinct xs" |
|
384 |
and pf: "xs >>= ys" |
|
385 |
shows "distinct ys" |
|
386 |
using dx pf by (clarsimp elim!: postfixE) |
|
387 |
||
388 |
lemma postfix_map: |
|
25355 | 389 |
assumes pf: "xs >>= ys" |
25299 | 390 |
shows "map f xs >>= map f ys" |
391 |
using pf by (auto elim!: postfixE intro: postfixI) |
|
392 |
||
393 |
lemma postfix_drop: |
|
394 |
"as >>= drop n as" |
|
395 |
unfolding postfix_def |
|
396 |
by (rule exI [where x = "take n as"]) simp |
|
397 |
||
398 |
lemma postfix_take: |
|
399 |
"xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys" |
|
400 |
by (clarsimp elim!: postfixE) |
|
401 |
||
25355 | 402 |
lemma parallelD1: |
25299 | 403 |
"x \<parallel> y \<Longrightarrow> \<not> x \<le> y" by blast |
404 |
||
25355 | 405 |
lemma parallelD2: |
25299 | 406 |
"x \<parallel> y \<Longrightarrow> \<not> y \<le> x" by blast |
25355 | 407 |
|
408 |
lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []" |
|
25299 | 409 |
unfolding parallel_def by simp |
25355 | 410 |
|
25299 | 411 |
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x" |
412 |
unfolding parallel_def by simp |
|
413 |
||
414 |
lemma Cons_parallelI1: |
|
415 |
"a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" by auto |
|
416 |
||
417 |
lemma Cons_parallelI2: |
|
25355 | 418 |
"\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs" |
25299 | 419 |
apply simp |
420 |
apply (rule parallelI) |
|
421 |
apply simp |
|
422 |
apply (erule parallelD1) |
|
423 |
apply simp |
|
424 |
apply (erule parallelD2) |
|
425 |
done |
|
426 |
||
427 |
lemma not_equal_is_parallel: |
|
428 |
assumes neq: "xs \<noteq> ys" |
|
429 |
and len: "length xs = length ys" |
|
430 |
shows "xs \<parallel> ys" |
|
431 |
using len neq |
|
25355 | 432 |
proof (induct rule: list_induct2) |
433 |
case 1 then show ?case by simp |
|
25299 | 434 |
next |
435 |
case (2 a as b bs) |
|
25355 | 436 |
have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact |
25299 | 437 |
|
438 |
show ?case |
|
439 |
proof (cases "a = b") |
|
25355 | 440 |
case True |
441 |
then have "as \<noteq> bs" using 2 by simp |
|
442 |
then show ?thesis by (rule Cons_parallelI2 [OF True ih]) |
|
25299 | 443 |
next |
444 |
case False |
|
25355 | 445 |
then show ?thesis by (rule Cons_parallelI1) |
25299 | 446 |
qed |
447 |
qed |
|
22178 | 448 |
|
25355 | 449 |
|
22178 | 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 |