author | wenzelm |
Thu, 06 May 2004 14:14:18 +0200 | |
changeset 14706 | 71590b7733b7 |
parent 14538 | 1d9d75a8efae |
child 14981 | e73f8140af78 |
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 |
11780 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
5 |
*) |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
6 |
|
14706 | 7 |
header {* List prefixes and postfixes *} |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
8 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
9 |
theory List_Prefix = Main: |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
10 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
11 |
subsection {* Prefix order on lists *} |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
12 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11987
diff
changeset
|
13 |
instance list :: (type) ord .. |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
14 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
15 |
defs (overloaded) |
10389 | 16 |
prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs" |
17 |
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
|
18 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11987
diff
changeset
|
19 |
instance list :: (type) order |
10389 | 20 |
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
|
21 |
|
10389 | 22 |
lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" |
23 |
by (unfold prefix_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
24 |
|
10389 | 25 |
lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C" |
26 |
by (unfold prefix_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
27 |
|
10870 | 28 |
lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" |
29 |
by (unfold strict_prefix_def prefix_def) blast |
|
30 |
||
31 |
lemma strict_prefixE' [elim?]: |
|
32 |
"xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C" |
|
33 |
proof - |
|
34 |
assume r: "!!z zs. ys = xs @ z # zs ==> C" |
|
35 |
assume "xs < ys" |
|
36 |
then obtain us where "ys = xs @ us" and "xs \<noteq> ys" |
|
37 |
by (unfold strict_prefix_def prefix_def) blast |
|
38 |
with r show ?thesis by (auto simp add: neq_Nil_conv) |
|
39 |
qed |
|
40 |
||
10389 | 41 |
lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" |
42 |
by (unfold strict_prefix_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
43 |
|
10389 | 44 |
lemma strict_prefixE [elim?]: |
45 |
"xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C" |
|
46 |
by (unfold strict_prefix_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
47 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
48 |
|
10389 | 49 |
subsection {* Basic properties of prefixes *} |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
50 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
51 |
theorem Nil_prefix [iff]: "[] \<le> xs" |
10389 | 52 |
by (simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
53 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
54 |
theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])" |
10389 | 55 |
by (induct xs) (simp_all add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
56 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
57 |
lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)" |
10389 | 58 |
proof |
59 |
assume "xs \<le> ys @ [y]" |
|
60 |
then obtain zs where zs: "ys @ [y] = xs @ zs" .. |
|
61 |
show "xs = ys @ [y] \<or> xs \<le> ys" |
|
62 |
proof (cases zs rule: rev_cases) |
|
63 |
assume "zs = []" |
|
64 |
with zs have "xs = ys @ [y]" by simp |
|
65 |
thus ?thesis .. |
|
66 |
next |
|
67 |
fix z zs' assume "zs = zs' @ [z]" |
|
68 |
with zs have "ys = xs @ zs'" by simp |
|
69 |
hence "xs \<le> ys" .. |
|
70 |
thus ?thesis .. |
|
71 |
qed |
|
72 |
next |
|
73 |
assume "xs = ys @ [y] \<or> xs \<le> ys" |
|
74 |
thus "xs \<le> ys @ [y]" |
|
75 |
proof |
|
76 |
assume "xs = ys @ [y]" |
|
77 |
thus ?thesis by simp |
|
78 |
next |
|
79 |
assume "xs \<le> ys" |
|
80 |
then obtain zs where "ys = xs @ zs" .. |
|
81 |
hence "ys @ [y] = xs @ (zs @ [y])" by simp |
|
82 |
thus ?thesis .. |
|
83 |
qed |
|
84 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
85 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
86 |
lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" |
10389 | 87 |
by (auto simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
88 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
89 |
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" |
10389 | 90 |
by (induct xs) simp_all |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
91 |
|
10389 | 92 |
lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" |
93 |
proof - |
|
94 |
have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) |
|
95 |
thus ?thesis by simp |
|
96 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
97 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
98 |
lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" |
10389 | 99 |
proof - |
100 |
assume "xs \<le> ys" |
|
101 |
then obtain us where "ys = xs @ us" .. |
|
102 |
hence "ys @ zs = xs @ (us @ zs)" by simp |
|
103 |
thus ?thesis .. |
|
104 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
105 |
|
14300 | 106 |
lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs" |
107 |
by(simp add:prefix_def) blast |
|
108 |
||
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
109 |
theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))" |
10389 | 110 |
by (cases xs) (auto simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
111 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
112 |
theorem prefix_append: |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
113 |
"(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
|
114 |
apply (induct zs rule: rev_induct) |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
115 |
apply force |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
116 |
apply (simp del: append_assoc add: append_assoc [symmetric]) |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
117 |
apply simp |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
118 |
apply blast |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
119 |
done |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
120 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
121 |
lemma append_one_prefix: |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
122 |
"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
|
123 |
apply (unfold prefix_def) |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
124 |
apply (auto simp add: nth_append) |
10389 | 125 |
apply (case_tac zs) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
126 |
apply auto |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
127 |
done |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
128 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
129 |
theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" |
10389 | 130 |
by (auto simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
131 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
132 |
|
14300 | 133 |
lemma prefix_same_cases: |
134 |
"\<lbrakk> (xs\<^isub>1::'a list) \<le> ys; xs\<^isub>2 \<le> ys \<rbrakk> \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1" |
|
135 |
apply(simp add:prefix_def) |
|
136 |
apply(erule exE)+ |
|
137 |
apply(simp add: append_eq_append_conv_if split:if_splits) |
|
138 |
apply(rule disjI2) |
|
139 |
apply(rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI) |
|
140 |
apply clarify |
|
141 |
apply(drule sym) |
|
142 |
apply(insert append_take_drop_id[of "length xs\<^isub>2" xs\<^isub>1]) |
|
143 |
apply simp |
|
144 |
apply(rule disjI1) |
|
145 |
apply(rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI) |
|
146 |
apply clarify |
|
147 |
apply(insert append_take_drop_id[of "length xs\<^isub>1" xs\<^isub>2]) |
|
148 |
apply simp |
|
149 |
done |
|
150 |
||
151 |
lemma set_mono_prefix: |
|
152 |
"xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys" |
|
153 |
by(fastsimp simp add:prefix_def) |
|
154 |
||
155 |
||
10389 | 156 |
subsection {* Parallel lists *} |
157 |
||
158 |
constdefs |
|
159 |
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) |
|
160 |
"xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
161 |
||
162 |
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
|
163 |
by (unfold parallel_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
164 |
|
10389 | 165 |
lemma parallelE [elim]: |
166 |
"xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C" |
|
167 |
by (unfold parallel_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
168 |
|
10389 | 169 |
theorem prefix_cases: |
170 |
"(xs \<le> ys ==> C) ==> |
|
10512 | 171 |
(ys < xs ==> C) ==> |
10389 | 172 |
(xs \<parallel> ys ==> C) ==> C" |
10512 | 173 |
by (unfold parallel_def strict_prefix_def) blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
174 |
|
10389 | 175 |
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" |
|
10408 | 177 |
proof (induct xs rule: rev_induct) |
11987 | 178 |
case Nil |
179 |
hence False by auto |
|
180 |
thus ?case .. |
|
10408 | 181 |
next |
11987 | 182 |
case (snoc x xs) |
183 |
show ?case |
|
10408 | 184 |
proof (rule prefix_cases) |
185 |
assume le: "xs \<le> ys" |
|
186 |
then obtain ys' where ys: "ys = xs @ ys'" .. |
|
187 |
show ?thesis |
|
188 |
proof (cases ys') |
|
189 |
assume "ys' = []" with ys have "xs = ys" by simp |
|
11987 | 190 |
with snoc have "[x] \<parallel> []" by auto |
10408 | 191 |
hence False by blast |
10389 | 192 |
thus ?thesis .. |
193 |
next |
|
10408 | 194 |
fix c cs assume ys': "ys' = c # cs" |
11987 | 195 |
with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) |
10408 | 196 |
hence "x \<noteq> c" by auto |
197 |
moreover have "xs @ [x] = xs @ x # []" by simp |
|
198 |
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) |
|
199 |
ultimately show ?thesis by blast |
|
10389 | 200 |
qed |
10408 | 201 |
next |
10512 | 202 |
assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) |
11987 | 203 |
with snoc have False by blast |
10408 | 204 |
thus ?thesis .. |
205 |
next |
|
206 |
assume "xs \<parallel> ys" |
|
11987 | 207 |
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" |
10408 | 208 |
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" |
209 |
by blast |
|
210 |
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp |
|
211 |
with neq ys show ?thesis by blast |
|
10389 | 212 |
qed |
213 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
214 |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
215 |
|
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
216 |
subsection {* Postfix order on lists *} |
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
217 |
|
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
218 |
constdefs |
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
219 |
postfix :: "'a list => 'a list => bool" ("(_/ >= _)" [51, 50] 50) |
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
220 |
"xs >= ys == \<exists>zs. xs = zs @ ys" |
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
221 |
|
14706 | 222 |
lemma postfix_refl [simp, intro!]: "xs >= xs" |
223 |
by (auto simp add: postfix_def) |
|
224 |
lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs" |
|
225 |
by (auto simp add: postfix_def) |
|
226 |
lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys" |
|
227 |
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
|
228 |
|
14706 | 229 |
lemma Nil_postfix [iff]: "xs >= []" |
230 |
by (simp add: postfix_def) |
|
231 |
lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])" |
|
232 |
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
|
233 |
|
14706 | 234 |
lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys" |
235 |
by (auto simp add: postfix_def) |
|
236 |
lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys" |
|
237 |
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
|
238 |
|
14706 | 239 |
lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs @ xs >= ys" |
240 |
by (auto simp add: postfix_def) |
|
241 |
lemma postfix_appendD: "xs >= zs @ ys \<Longrightarrow> xs >= ys" |
|
242 |
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
|
243 |
|
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
244 |
lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs" |
14706 | 245 |
by (induct zs, auto) |
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
246 |
lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs" |
14706 | 247 |
by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma) |
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
248 |
|
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
249 |
lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys" |
14706 | 250 |
by (induct zs, auto intro!: postfix_appendI postfix_ConsI) |
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
251 |
lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys" |
14706 | 252 |
by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma) |
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
253 |
|
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
254 |
lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)" |
14706 | 255 |
apply (unfold prefix_def postfix_def, safe) |
256 |
apply (rule_tac x = "rev zs" in exI, simp) |
|
257 |
apply (rule_tac x = "rev zs" in exI) |
|
258 |
apply (rule rev_is_rev_conv [THEN iffD1], simp) |
|
259 |
done |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
260 |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
261 |
end |