author | berghofe |
Wed, 11 Jul 2007 11:28:13 +0200 | |
changeset 23755 | 1c4672d130b1 |
parent 23394 | 474ff28210c0 |
child 25299 | c3542f70b0fd |
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 |
|
158 |
||
10389 | 159 |
subsection {* Parallel lists *} |
160 |
||
19086 | 161 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset
|
162 |
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) where |
19086 | 163 |
"(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)" |
10389 | 164 |
|
165 |
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
|
18730 | 166 |
unfolding parallel_def by blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
167 |
|
10389 | 168 |
lemma parallelE [elim]: |
21305 | 169 |
assumes "xs \<parallel> ys" |
170 |
obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
23394 | 171 |
using assms unfolding parallel_def by blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
172 |
|
10389 | 173 |
theorem prefix_cases: |
21305 | 174 |
obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys" |
18730 | 175 |
unfolding parallel_def strict_prefix_def by blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
176 |
|
10389 | 177 |
theorem parallel_decomp: |
178 |
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" |
|
10408 | 179 |
proof (induct xs rule: rev_induct) |
11987 | 180 |
case Nil |
23254 | 181 |
then have False by auto |
182 |
then show ?case .. |
|
10408 | 183 |
next |
11987 | 184 |
case (snoc x xs) |
185 |
show ?case |
|
10408 | 186 |
proof (rule prefix_cases) |
187 |
assume le: "xs \<le> ys" |
|
188 |
then obtain ys' where ys: "ys = xs @ ys'" .. |
|
189 |
show ?thesis |
|
190 |
proof (cases ys') |
|
191 |
assume "ys' = []" with ys have "xs = ys" by simp |
|
11987 | 192 |
with snoc have "[x] \<parallel> []" by auto |
23254 | 193 |
then have False by blast |
194 |
then show ?thesis .. |
|
10389 | 195 |
next |
10408 | 196 |
fix c cs assume ys': "ys' = c # cs" |
11987 | 197 |
with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) |
23254 | 198 |
then have "x \<noteq> c" by auto |
10408 | 199 |
moreover have "xs @ [x] = xs @ x # []" by simp |
200 |
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) |
|
201 |
ultimately show ?thesis by blast |
|
10389 | 202 |
qed |
10408 | 203 |
next |
23254 | 204 |
assume "ys < xs" then have "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) |
11987 | 205 |
with snoc have False by blast |
23254 | 206 |
then show ?thesis .. |
10408 | 207 |
next |
208 |
assume "xs \<parallel> ys" |
|
11987 | 209 |
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" |
10408 | 210 |
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" |
211 |
by blast |
|
212 |
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp |
|
213 |
with neq ys show ?thesis by blast |
|
10389 | 214 |
qed |
215 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
216 |
|
14538
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 |
subsection {* Postfix order on lists *} |
17201 | 219 |
|
19086 | 220 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21305
diff
changeset
|
221 |
postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) where |
19086 | 222 |
"(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
|
223 |
|
21305 | 224 |
lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" |
225 |
unfolding postfix_def by blast |
|
226 |
||
227 |
lemma postfixE [elim?]: |
|
228 |
assumes "xs >>= ys" |
|
229 |
obtains zs where "xs = zs @ ys" |
|
23394 | 230 |
using assms unfolding postfix_def by blast |
21305 | 231 |
|
232 |
lemma postfix_refl [iff]: "xs >>= xs" |
|
14706 | 233 |
by (auto simp add: postfix_def) |
17201 | 234 |
lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" |
14706 | 235 |
by (auto simp add: postfix_def) |
17201 | 236 |
lemma postfix_antisym: "\<lbrakk>xs >>= ys; ys >>= xs\<rbrakk> \<Longrightarrow> xs = ys" |
14706 | 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 |
|
17201 | 239 |
lemma Nil_postfix [iff]: "xs >>= []" |
14706 | 240 |
by (simp add: postfix_def) |
17201 | 241 |
lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" |
21305 | 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 |
|
17201 | 244 |
lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" |
14706 | 245 |
by (auto simp add: postfix_def) |
17201 | 246 |
lemma postfix_ConsD: "xs >>= y#ys \<Longrightarrow> xs >>= ys" |
14706 | 247 |
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
|
248 |
|
17201 | 249 |
lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" |
14706 | 250 |
by (auto simp add: postfix_def) |
17201 | 251 |
lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" |
21305 | 252 |
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
|
253 |
|
21305 | 254 |
lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs" |
255 |
proof - |
|
256 |
assume "xs >>= ys" |
|
257 |
then obtain zs where "xs = zs @ ys" .. |
|
258 |
then show ?thesis by (induct zs) auto |
|
259 |
qed |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
260 |
|
21305 | 261 |
lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" |
262 |
proof - |
|
263 |
assume "x#xs >>= y#ys" |
|
264 |
then obtain zs where "x#xs = zs @ y#ys" .. |
|
265 |
then show ?thesis |
|
266 |
by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) |
|
267 |
qed |
|
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset
|
268 |
|
21305 | 269 |
lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs" |
270 |
proof |
|
271 |
assume "xs >>= ys" |
|
272 |
then obtain zs where "xs = zs @ ys" .. |
|
273 |
then have "rev xs = rev ys @ rev zs" by simp |
|
274 |
then show "rev ys <= rev xs" .. |
|
275 |
next |
|
276 |
assume "rev ys <= rev xs" |
|
277 |
then obtain zs where "rev xs = rev ys @ zs" .. |
|
278 |
then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp |
|
279 |
then have "xs = rev zs @ ys" by simp |
|
280 |
then show "xs >>= ys" .. |
|
281 |
qed |
|
17201 | 282 |
|
22178 | 283 |
|
284 |
subsection {* Exeuctable code *} |
|
285 |
||
286 |
lemma less_eq_code [code func]: |
|
287 |
"([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True" |
|
288 |
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False" |
|
289 |
"(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys" |
|
290 |
by simp_all |
|
291 |
||
292 |
lemma less_code [code func]: |
|
293 |
"xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False" |
|
294 |
"[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True" |
|
295 |
"(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys" |
|
296 |
unfolding strict_prefix_def by auto |
|
297 |
||
298 |
lemmas [code func] = postfix_to_prefix |
|
299 |
||
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
300 |
end |