author  nipkow 
Wed, 18 Aug 2004 11:09:40 +0200  
changeset 15140  322485b816ac 
parent 15131  c69542757a4d 
child 15355  0de05d104060 
permissions  rwrr 
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" 
24 
by (unfold prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

25 

10389  26 
lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C" 
27 
by (unfold prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

28 

10870  29 
lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" 
30 
by (unfold strict_prefix_def prefix_def) blast 

31 

32 
lemma strict_prefixE' [elim?]: 

33 
"xs < ys ==> (!!z zs. ys = xs @ z # zs ==> C) ==> C" 

34 
proof  

35 
assume r: "!!z zs. ys = xs @ z # zs ==> C" 

36 
assume "xs < ys" 

37 
then obtain us where "ys = xs @ us" and "xs \<noteq> ys" 

38 
by (unfold strict_prefix_def prefix_def) blast 

39 
with r show ?thesis by (auto simp add: neq_Nil_conv) 

40 
qed 

41 

10389  42 
lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" 
43 
by (unfold strict_prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

44 

10389  45 
lemma strict_prefixE [elim?]: 
46 
"xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C" 

47 
by (unfold strict_prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

48 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

49 

10389  50 
subsection {* Basic properties of prefixes *} 
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 
theorem Nil_prefix [iff]: "[] \<le> xs" 
10389  53 
by (simp add: prefix_def) 
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 prefix_Nil [simp]: "(xs \<le> []) = (xs = [])" 
10389  56 
by (induct xs) (simp_all 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 
lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)" 
10389  59 
proof 
60 
assume "xs \<le> ys @ [y]" 

61 
then obtain zs where zs: "ys @ [y] = xs @ zs" .. 

62 
show "xs = ys @ [y] \<or> xs \<le> ys" 

63 
proof (cases zs rule: rev_cases) 

64 
assume "zs = []" 

65 
with zs have "xs = ys @ [y]" by simp 

66 
thus ?thesis .. 

67 
next 

68 
fix z zs' assume "zs = zs' @ [z]" 

69 
with zs have "ys = xs @ zs'" by simp 

70 
hence "xs \<le> ys" .. 

71 
thus ?thesis .. 

72 
qed 

73 
next 

74 
assume "xs = ys @ [y] \<or> xs \<le> ys" 

75 
thus "xs \<le> ys @ [y]" 

76 
proof 

77 
assume "xs = ys @ [y]" 

78 
thus ?thesis by simp 

79 
next 

80 
assume "xs \<le> ys" 

81 
then obtain zs where "ys = xs @ zs" .. 

82 
hence "ys @ [y] = xs @ (zs @ [y])" by simp 

83 
thus ?thesis .. 

84 
qed 

85 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

86 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

87 
lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" 
10389  88 
by (auto simp add: prefix_def) 
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 same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" 
10389  91 
by (induct xs) simp_all 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

92 

10389  93 
lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" 
94 
proof  

95 
have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) 

96 
thus ?thesis by simp 

97 
qed 

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 prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" 
10389  100 
proof  
101 
assume "xs \<le> ys" 

102 
then obtain us where "ys = xs @ us" .. 

103 
hence "ys @ zs = xs @ (us @ zs)" by simp 

104 
thus ?thesis .. 

105 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

106 

14300  107 
lemma append_prefixD: "xs @ ys \<le> zs \<Longrightarrow> xs \<le> zs" 
108 
by(simp add:prefix_def) blast 

109 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

110 
theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))" 
10389  111 
by (cases xs) (auto simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

112 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

113 
theorem prefix_append: 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

114 
"(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

115 
apply (induct zs rule: rev_induct) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

116 
apply force 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

117 
apply (simp del: append_assoc add: append_assoc [symmetric]) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

118 
apply simp 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

119 
apply blast 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

120 
done 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

121 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

122 
lemma append_one_prefix: 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

123 
"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

124 
apply (unfold prefix_def) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

125 
apply (auto simp add: nth_append) 
10389  126 
apply (case_tac zs) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

127 
apply auto 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

128 
done 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

129 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

130 
theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" 
10389  131 
by (auto simp add: prefix_def) 
10330
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 

14300  134 
lemma prefix_same_cases: 
135 
"\<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" 

136 
apply(simp add:prefix_def) 

137 
apply(erule exE)+ 

138 
apply(simp add: append_eq_append_conv_if split:if_splits) 

139 
apply(rule disjI2) 

140 
apply(rule_tac x = "drop (size xs\<^isub>2) xs\<^isub>1" in exI) 

141 
apply clarify 

142 
apply(drule sym) 

143 
apply(insert append_take_drop_id[of "length xs\<^isub>2" xs\<^isub>1]) 

144 
apply simp 

145 
apply(rule disjI1) 

146 
apply(rule_tac x = "drop (size xs\<^isub>1) xs\<^isub>2" in exI) 

147 
apply clarify 

148 
apply(insert append_take_drop_id[of "length xs\<^isub>1" xs\<^isub>2]) 

149 
apply simp 

150 
done 

151 

152 
lemma set_mono_prefix: 

153 
"xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys" 

154 
by(fastsimp simp add:prefix_def) 

155 

156 

10389  157 
subsection {* Parallel lists *} 
158 

159 
constdefs 

160 
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) 

161 
"xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs" 

162 

163 
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" 

164 
by (unfold parallel_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

165 

10389  166 
lemma parallelE [elim]: 
167 
"xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C" 

168 
by (unfold parallel_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

169 

10389  170 
theorem prefix_cases: 
171 
"(xs \<le> ys ==> C) ==> 

10512  172 
(ys < xs ==> C) ==> 
10389  173 
(xs \<parallel> ys ==> C) ==> C" 
10512  174 
by (unfold parallel_def strict_prefix_def) blast 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

175 

10389  176 
theorem parallel_decomp: 
177 
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 

10408  178 
proof (induct xs rule: rev_induct) 
11987  179 
case Nil 
180 
hence False by auto 

181 
thus ?case .. 

10408  182 
next 
11987  183 
case (snoc x xs) 
184 
show ?case 

10408  185 
proof (rule prefix_cases) 
186 
assume le: "xs \<le> ys" 

187 
then obtain ys' where ys: "ys = xs @ ys'" .. 

188 
show ?thesis 

189 
proof (cases ys') 

190 
assume "ys' = []" with ys have "xs = ys" by simp 

11987  191 
with snoc have "[x] \<parallel> []" by auto 
10408  192 
hence False by blast 
10389  193 
thus ?thesis .. 
194 
next 

10408  195 
fix c cs assume ys': "ys' = c # cs" 
11987  196 
with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) 
10408  197 
hence "x \<noteq> c" by auto 
198 
moreover have "xs @ [x] = xs @ x # []" by simp 

199 
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) 

200 
ultimately show ?thesis by blast 

10389  201 
qed 
10408  202 
next 
10512  203 
assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def) 
11987  204 
with snoc have False by blast 
10408  205 
thus ?thesis .. 
206 
next 

207 
assume "xs \<parallel> ys" 

11987  208 
with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 
10408  209 
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 
210 
by blast 

211 
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp 

212 
with neq ys show ?thesis by blast 

10389  213 
qed 
214 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

215 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

216 

1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

217 
subsection {* Postfix order on lists *} 
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

218 

1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

219 
constdefs 
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

220 
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

221 
"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

222 

14706  223 
lemma postfix_refl [simp, intro!]: "xs >= xs" 
224 
by (auto simp add: postfix_def) 

225 
lemma postfix_trans: "\<lbrakk>xs >= ys; ys >= zs\<rbrakk> \<Longrightarrow> xs >= zs" 

226 
by (auto simp add: postfix_def) 

227 
lemma postfix_antisym: "\<lbrakk>xs >= ys; ys >= xs\<rbrakk> \<Longrightarrow> xs = ys" 

228 
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

229 

14706  230 
lemma Nil_postfix [iff]: "xs >= []" 
231 
by (simp add: postfix_def) 

232 
lemma postfix_Nil [simp]: "([] >= xs) = (xs = [])" 

233 
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

234 

14706  235 
lemma postfix_ConsI: "xs >= ys \<Longrightarrow> x#xs >= ys" 
236 
by (auto simp add: postfix_def) 

237 
lemma postfix_ConsD: "xs >= y#ys \<Longrightarrow> xs >= ys" 

238 
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

239 

14706  240 
lemma postfix_appendI: "xs >= ys \<Longrightarrow> zs @ xs >= ys" 
241 
by (auto simp add: postfix_def) 

242 
lemma postfix_appendD: "xs >= zs @ ys \<Longrightarrow> xs >= ys" 

243 
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

244 

1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

245 
lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs" 
14706  246 
by (induct zs, auto) 
14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

247 
lemma postfix_is_subset: "xs >= ys \<Longrightarrow> set ys \<subseteq> set xs" 
14706  248 
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

249 

1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

250 
lemma postfix_ConsD2_lemma [rule_format]: "x#xs = zs @ y#ys \<longrightarrow> xs >= ys" 
14706  251 
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

252 
lemma postfix_ConsD2: "x#xs >= y#ys \<Longrightarrow> xs >= ys" 
14706  253 
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

254 

1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

255 
lemma postfix2prefix: "(xs >= ys) = (rev ys <= rev xs)" 
14706  256 
apply (unfold prefix_def postfix_def, safe) 
257 
apply (rule_tac x = "rev zs" in exI, simp) 

258 
apply (rule_tac x = "rev zs" in exI) 

259 
apply (rule rev_is_rev_conv [THEN iffD1], simp) 

260 
done 

14538
1d9d75a8efae
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
oheimb
parents:
14300
diff
changeset

261 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

262 
end 