author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 11987 | bf31b35949ce |
child 14300 | bf8b8c9425c3 |
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 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
7 |
header {* |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
8 |
\title{List prefixes} |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
9 |
\author{Tobias Nipkow and Markus Wenzel} |
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 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
12 |
theory List_Prefix = Main: |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
13 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
14 |
subsection {* Prefix order on lists *} |
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
15 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11987
diff
changeset
|
16 |
instance list :: (type) ord .. |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
17 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
18 |
defs (overloaded) |
10389 | 19 |
prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs" |
20 |
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
|
21 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11987
diff
changeset
|
22 |
instance list :: (type) order |
10389 | 23 |
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
|
24 |
|
10389 | 25 |
lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" |
26 |
by (unfold prefix_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
27 |
|
10389 | 28 |
lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C" |
29 |
by (unfold prefix_def) 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" |
32 |
by (unfold strict_prefix_def prefix_def) blast |
|
33 |
||
34 |
lemma strict_prefixE' [elim?]: |
|
35 |
"xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C" |
|
36 |
proof - |
|
37 |
assume r: "!!z zs. ys = xs @ z # zs ==> C" |
|
38 |
assume "xs < ys" |
|
39 |
then obtain us where "ys = xs @ us" and "xs \<noteq> ys" |
|
40 |
by (unfold strict_prefix_def prefix_def) blast |
|
41 |
with r show ?thesis by (auto simp add: neq_Nil_conv) |
|
42 |
qed |
|
43 |
||
10389 | 44 |
lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" |
45 |
by (unfold strict_prefix_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
46 |
|
10389 | 47 |
lemma strict_prefixE [elim?]: |
48 |
"xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C" |
|
49 |
by (unfold strict_prefix_def) blast |
|
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 |
|
10389 | 52 |
subsection {* Basic properties of prefixes *} |
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 Nil_prefix [iff]: "[] \<le> xs" |
10389 | 55 |
by (simp 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 |
theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])" |
10389 | 58 |
by (induct xs) (simp_all add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
59 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
60 |
lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)" |
10389 | 61 |
proof |
62 |
assume "xs \<le> ys @ [y]" |
|
63 |
then obtain zs where zs: "ys @ [y] = xs @ zs" .. |
|
64 |
show "xs = ys @ [y] \<or> xs \<le> ys" |
|
65 |
proof (cases zs rule: rev_cases) |
|
66 |
assume "zs = []" |
|
67 |
with zs have "xs = ys @ [y]" by simp |
|
68 |
thus ?thesis .. |
|
69 |
next |
|
70 |
fix z zs' assume "zs = zs' @ [z]" |
|
71 |
with zs have "ys = xs @ zs'" by simp |
|
72 |
hence "xs \<le> ys" .. |
|
73 |
thus ?thesis .. |
|
74 |
qed |
|
75 |
next |
|
76 |
assume "xs = ys @ [y] \<or> xs \<le> ys" |
|
77 |
thus "xs \<le> ys @ [y]" |
|
78 |
proof |
|
79 |
assume "xs = ys @ [y]" |
|
80 |
thus ?thesis by simp |
|
81 |
next |
|
82 |
assume "xs \<le> ys" |
|
83 |
then obtain zs where "ys = xs @ zs" .. |
|
84 |
hence "ys @ [y] = xs @ (zs @ [y])" by simp |
|
85 |
thus ?thesis .. |
|
86 |
qed |
|
87 |
qed |
|
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 Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" |
10389 | 90 |
by (auto simp add: prefix_def) |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
91 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
92 |
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" |
10389 | 93 |
by (induct xs) simp_all |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
94 |
|
10389 | 95 |
lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" |
96 |
proof - |
|
97 |
have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) |
|
98 |
thus ?thesis by simp |
|
99 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
100 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
101 |
lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" |
10389 | 102 |
proof - |
103 |
assume "xs \<le> ys" |
|
104 |
then obtain us where "ys = xs @ us" .. |
|
105 |
hence "ys @ zs = xs @ (us @ zs)" by simp |
|
106 |
thus ?thesis .. |
|
107 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
108 |
|
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 |
|
10389 | 133 |
subsection {* Parallel lists *} |
134 |
||
135 |
constdefs |
|
136 |
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) |
|
137 |
"xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
138 |
||
139 |
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" |
|
140 |
by (unfold parallel_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
141 |
|
10389 | 142 |
lemma parallelE [elim]: |
143 |
"xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C" |
|
144 |
by (unfold parallel_def) blast |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
145 |
|
10389 | 146 |
theorem prefix_cases: |
147 |
"(xs \<le> ys ==> C) ==> |
|
10512 | 148 |
(ys < xs ==> C) ==> |
10389 | 149 |
(xs \<parallel> ys ==> C) ==> C" |
10512 | 150 |
by (unfold parallel_def strict_prefix_def) blast |
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
151 |
|
10389 | 152 |
theorem parallel_decomp: |
153 |
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" |
|
10408 | 154 |
proof (induct xs rule: rev_induct) |
11987 | 155 |
case Nil |
156 |
hence False by auto |
|
157 |
thus ?case .. |
|
10408 | 158 |
next |
11987 | 159 |
case (snoc x xs) |
160 |
show ?case |
|
10408 | 161 |
proof (rule prefix_cases) |
162 |
assume le: "xs \<le> ys" |
|
163 |
then obtain ys' where ys: "ys = xs @ ys'" .. |
|
164 |
show ?thesis |
|
165 |
proof (cases ys') |
|
166 |
assume "ys' = []" with ys have "xs = ys" by simp |
|
11987 | 167 |
with snoc have "[x] \<parallel> []" by auto |
10408 | 168 |
hence False by blast |
10389 | 169 |
thus ?thesis .. |
170 |
next |
|
10408 | 171 |
fix c cs assume ys': "ys' = c # cs" |
11987 | 172 |
with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) |
10408 | 173 |
hence "x \<noteq> c" by auto |
174 |
moreover have "xs @ [x] = xs @ x # []" by simp |
|
175 |
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) |
|
176 |
ultimately show ?thesis by blast |
|
10389 | 177 |
qed |
10408 | 178 |
next |
10512 | 179 |
assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) |
11987 | 180 |
with snoc have False by blast |
10408 | 181 |
thus ?thesis .. |
182 |
next |
|
183 |
assume "xs \<parallel> ys" |
|
11987 | 184 |
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" |
10408 | 185 |
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" |
186 |
by blast |
|
187 |
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp |
|
188 |
with neq ys show ?thesis by blast |
|
10389 | 189 |
qed |
190 |
qed |
|
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
191 |
|
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset
|
192 |
end |