author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58871  c399ae4b836f 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26060
diff
changeset

1 
(* Title: ZF/UNITY/GenPrefix.thy 
12197  2 
Author: Sidi O Ehmety, Cambridge University Computer Laboratory 
3 
Copyright 2001 University of Cambridge 

4 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26060
diff
changeset

5 
<xs,ys>:gen_prefix(r) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26060
diff
changeset

6 
if ys = xs' @ zs where length(xs) = length(xs') 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26060
diff
changeset

7 
and corresponding elements of xs, xs' are pairwise related by r 
12197  8 

9 
Based on Lex/Prefix 

10 
*) 

11 

15634  12 
header{*Charpentier's Generalized Prefix Relation*} 
13 

14 
theory GenPrefix 

26060  15 
imports Main 
15634  16 
begin 
12197  17 

24893  18 
definition (*really belongs in ZF/Trancl*) 
19 
part_order :: "[i, i] => o" where 

14055  20 
"part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)" 
21 

12197  22 
consts 
23 
gen_prefix :: "[i, i] => i" 

24892  24 

12197  25 
inductive 
26 
(* Parameter A is the domain of zs's elements *) 

24892  27 

46823  28 
domains "gen_prefix(A, r)" \<subseteq> "list(A)*list(A)" 
24892  29 

15634  30 
intros 
31 
Nil: "<[],[]>:gen_prefix(A, r)" 

12197  32 

46953  33 
prepend: "[ <xs,ys>:gen_prefix(A, r); <x,y>:r; x \<in> A; y \<in> A ] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26060
diff
changeset

34 
==> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)" 
12197  35 

15634  36 
append: "[ <xs,ys>:gen_prefix(A, r); zs:list(A) ] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26060
diff
changeset

37 
==> <xs, ys@zs>:gen_prefix(A, r)" 
15634  38 
type_intros app_type list.Nil list.Cons 
12197  39 

24893  40 
definition 
41 
prefix :: "i=>i" where 

12197  42 
"prefix(A) == gen_prefix(A, id(A))" 
43 

24893  44 
definition 
45 
strict_prefix :: "i=>i" where 

12197  46 
"strict_prefix(A) == prefix(A)  id(list(A))" 
47 

24892  48 

49 
(* less or equal and greater or equal over prefixes *) 

50 

51 
abbreviation 

52 
pfixLe :: "[i, i] => o" (infixl "pfixLe" 50) where 

53 
"xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)" 

12197  54 

24892  55 
abbreviation 
56 
pfixGe :: "[i, i] => o" (infixl "pfixGe" 50) where 

57 
"xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)" 

12197  58 

24892  59 

60 
lemma reflD: 

15634  61 
"[ refl(A, r); x \<in> A ] ==> <x,x>:r" 
62 
apply (unfold refl_def, auto) 

63 
done 

64 

65 
(*** preliminary lemmas ***) 

66 

67 
lemma Nil_gen_prefix: "xs \<in> list(A) ==> <[], xs> \<in> gen_prefix(A, r)" 

68 
by (drule gen_prefix.append [OF gen_prefix.Nil], simp) 

69 
declare Nil_gen_prefix [simp] 

70 

71 

72 
lemma gen_prefix_length_le: "<xs,ys> \<in> gen_prefix(A, r) ==> length(xs) \<le> length(ys)" 

73 
apply (erule gen_prefix.induct) 

74 
apply (subgoal_tac [3] "ys \<in> list (A) ") 

75 
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] 

76 
intro: le_trans simp add: length_app) 

77 
done 

78 

79 

80 
lemma Cons_gen_prefix_aux: 

24892  81 
"[ <xs', ys'> \<in> gen_prefix(A, r) ] 
46823  82 
==> (\<forall>x xs. x \<in> A \<longrightarrow> xs'= Cons(x,xs) \<longrightarrow> 
24892  83 
(\<exists>y ys. y \<in> A & ys' = Cons(y,ys) & 
15634  84 
<x,y>:r & <xs, ys> \<in> gen_prefix(A, r)))" 
85 
apply (erule gen_prefix.induct) 

24892  86 
prefer 3 apply (force intro: gen_prefix.append, auto) 
15634  87 
done 
88 

89 
lemma Cons_gen_prefixE: 

24892  90 
"[ <Cons(x,xs), zs> \<in> gen_prefix(A, r); 
91 
!!y ys. [zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r; 

15634  92 
<xs,ys> \<in> gen_prefix(A, r) ] ==> P ] ==> P" 
24892  93 
apply (frule gen_prefix.dom_subset [THEN subsetD], auto) 
94 
apply (blast dest: Cons_gen_prefix_aux) 

15634  95 
done 
96 
declare Cons_gen_prefixE [elim!] 

97 

24892  98 
lemma Cons_gen_prefix_Cons: 
99 
"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r)) 

46823  100 
\<longleftrightarrow> (x \<in> A & y \<in> A & <x,y>:r & <xs,ys> \<in> gen_prefix(A, r))" 
15634  101 
apply (auto intro: gen_prefix.prepend) 
102 
done 

103 
declare Cons_gen_prefix_Cons [iff] 

104 

105 
(** Monotonicity of gen_prefix **) 

106 

46823  107 
lemma gen_prefix_mono2: "r<=s ==> gen_prefix(A, r) \<subseteq> gen_prefix(A, s)" 
15634  108 
apply clarify 
109 
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 

110 
apply (erule rev_mp) 

111 
apply (erule gen_prefix.induct) 

112 
apply (auto intro: gen_prefix.append) 

113 
done 

114 

46823  115 
lemma gen_prefix_mono1: "A<=B ==>gen_prefix(A, r) \<subseteq> gen_prefix(B, r)" 
15634  116 
apply clarify 
117 
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 

118 
apply (erule rev_mp) 

119 
apply (erule_tac P = "y \<in> list (A) " in rev_mp) 

120 
apply (erule_tac P = "xa \<in> list (A) " in rev_mp) 

121 
apply (erule gen_prefix.induct) 

122 
apply (simp (no_asm_simp)) 

123 
apply clarify 

124 
apply (erule ConsE)+ 

125 
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] 

126 
intro: gen_prefix.append list_mono [THEN subsetD]) 

127 
done 

128 

46823  129 
lemma gen_prefix_mono: "[ A \<subseteq> B; r \<subseteq> s ] ==> gen_prefix(A, r) \<subseteq> gen_prefix(B, s)" 
15634  130 
apply (rule subset_trans) 
131 
apply (rule gen_prefix_mono1) 

132 
apply (rule_tac [2] gen_prefix_mono2, auto) 

133 
done 

134 

135 
(*** gen_prefix order ***) 

136 

137 
(* reflexivity *) 

138 
lemma refl_gen_prefix: "refl(A, r) ==> refl(list(A), gen_prefix(A, r))" 

139 
apply (unfold refl_def, auto) 

140 
apply (induct_tac "x", auto) 

141 
done 

142 
declare refl_gen_prefix [THEN reflD, simp] 

143 

144 
(* Transitivity *) 

145 
(* A lemma for proving gen_prefix_trans_comp *) 

146 

24892  147 
lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==> 
46823  148 
\<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) \<longrightarrow> <xs, zs>: gen_prefix(A, r)" 
15634  149 
apply (erule list.induct) 
150 
apply (auto dest: gen_prefix.dom_subset [THEN subsetD]) 

151 
done 

152 

153 
(* Lemma proving transitivity and more*) 

154 

155 
lemma gen_prefix_trans_comp [rule_format (no_asm)]: 

24892  156 
"<x, y>: gen_prefix(A, r) ==> 
46823  157 
(\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)\<longrightarrow><x, z> \<in> gen_prefix(A, s O r))" 
15634  158 
apply (erule gen_prefix.induct) 
159 
apply (auto elim: ConsE simp add: Nil_gen_prefix) 

160 
apply (subgoal_tac "ys \<in> list (A) ") 

161 
prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD]) 

162 
apply (drule_tac xs = ys and r = s in append_gen_prefix, auto) 

163 
done 

164 

46823  165 
lemma trans_comp_subset: "trans(r) ==> r O r \<subseteq> r" 
15634  166 
by (auto dest: transD) 
167 

168 
lemma trans_gen_prefix: "trans(r) ==> trans(gen_prefix(A,r))" 

169 
apply (simp (no_asm) add: trans_def) 

170 
apply clarify 

171 
apply (rule trans_comp_subset [THEN gen_prefix_mono2, THEN subsetD], assumption) 

172 
apply (rule gen_prefix_trans_comp) 

173 
apply (auto dest: gen_prefix.dom_subset [THEN subsetD]) 

174 
done 

175 

24892  176 
lemma trans_on_gen_prefix: 
15634  177 
"trans(r) ==> trans[list(A)](gen_prefix(A, r))" 
178 
apply (drule_tac A = A in trans_gen_prefix) 

179 
apply (unfold trans_def trans_on_def, blast) 

180 
done 

181 

182 
lemma prefix_gen_prefix_trans: 

24892  183 
"[ <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A ] 
15634  184 
==> <x, z> \<in> gen_prefix(A, r)" 
185 
apply (unfold prefix_def) 

186 
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst]) 

187 
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+ 

188 
done 

189 

190 

24892  191 
lemma gen_prefix_prefix_trans: 
192 
"[ <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A ] 

15634  193 
==> <x, z> \<in> gen_prefix(A, r)" 
194 
apply (unfold prefix_def) 

195 
apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst]) 

196 
apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+ 

197 
done 

198 

199 
(** Antisymmetry **) 

200 

46823  201 
lemma nat_le_lemma [rule_format]: "n \<in> nat ==> \<forall>b \<in> nat. n #+ b \<le> n \<longrightarrow> b = 0" 
15634  202 
by (induct_tac "n", auto) 
203 

204 
lemma antisym_gen_prefix: "antisym(r) ==> antisym(gen_prefix(A, r))" 

205 
apply (simp (no_asm) add: antisym_def) 

206 
apply (rule impI [THEN allI, THEN allI]) 

24892  207 
apply (erule gen_prefix.induct, blast) 
15634  208 
apply (simp add: antisym_def, blast) 
209 
txt{*append case is hardest*} 

210 
apply clarify 

211 
apply (subgoal_tac "length (zs) = 0") 

212 
apply (subgoal_tac "ys \<in> list (A) ") 

213 
prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD]) 

214 
apply (drule_tac psi = "<ys @ zs, xs> \<in> gen_prefix (A,r) " in asm_rl) 

215 
apply simp 

216 
apply (subgoal_tac "length (ys @ zs) = length (ys) #+ length (zs) &ys \<in> list (A) &xs \<in> list (A) ") 

217 
prefer 2 apply (blast intro: length_app dest: gen_prefix.dom_subset [THEN subsetD]) 

218 
apply (drule gen_prefix_length_le)+ 

219 
apply clarify 

220 
apply simp 

221 
apply (drule_tac j = "length (xs) " in le_trans) 

222 
apply blast 

223 
apply (auto intro: nat_le_lemma) 

224 
done 

225 

226 
(*** recursion equations ***) 

227 

46823  228 
lemma gen_prefix_Nil: "xs \<in> list(A) ==> <xs, []> \<in> gen_prefix(A,r) \<longleftrightarrow> (xs = [])" 
15634  229 
by (induct_tac "xs", auto) 
230 
declare gen_prefix_Nil [simp] 

231 

24892  232 
lemma same_gen_prefix_gen_prefix: 
233 
"[ refl(A, r); xs \<in> list(A) ] ==> 

46823  234 
<xs@ys, xs@zs>: gen_prefix(A, r) \<longleftrightarrow> <ys,zs> \<in> gen_prefix(A, r)" 
15634  235 
apply (unfold refl_def) 
236 
apply (induct_tac "xs") 

237 
apply (simp_all (no_asm_simp)) 

238 
done 

239 
declare same_gen_prefix_gen_prefix [simp] 

240 

24892  241 
lemma gen_prefix_Cons: "[ xs \<in> list(A); ys \<in> list(A); y \<in> A ] ==> 
46823  242 
<xs, Cons(y,ys)> \<in> gen_prefix(A,r) \<longleftrightarrow> 
15634  243 
(xs=[]  (\<exists>z zs. xs=Cons(z,zs) & z \<in> A & <z,y>:r & <zs,ys> \<in> gen_prefix(A,r)))" 
244 
apply (induct_tac "xs", auto) 

245 
done 

246 

24892  247 
lemma gen_prefix_take_append: "[ refl(A,r); <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) ] 
15634  248 
==> <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)" 
249 
apply (erule gen_prefix.induct) 

250 
apply (simp (no_asm_simp)) 

251 
apply (frule_tac [!] gen_prefix.dom_subset [THEN subsetD], auto) 

252 
apply (frule gen_prefix_length_le) 

253 
apply (subgoal_tac "take (length (xs), ys) \<in> list (A) ") 

254 
apply (simp_all (no_asm_simp) add: diff_is_0_iff [THEN iffD2] take_type) 

255 
done 

256 

24892  257 
lemma gen_prefix_append_both: "[ refl(A, r); <xs,ys> \<in> gen_prefix(A,r); 
258 
length(xs) = length(ys); zs \<in> list(A) ] 

15634  259 
==> <xs@zs, ys @ zs> \<in> gen_prefix(A, r)" 
260 
apply (drule_tac zs = zs in gen_prefix_take_append, assumption+) 

261 
apply (subgoal_tac "take (length (xs), ys) =ys") 

262 
apply (auto intro!: take_all dest: gen_prefix.dom_subset [THEN subsetD]) 

263 
done 

264 

265 
(*NOT suitable for rewriting since [y] has the form y#ys*) 

266 
lemma append_cons_conv: "xs \<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys" 

267 
by (auto simp add: app_assoc) 

268 

269 
lemma append_one_gen_prefix_lemma [rule_format]: 

24892  270 
"[ <xs,ys> \<in> gen_prefix(A, r); refl(A, r) ] 
46823  271 
==> length(xs) < length(ys) \<longrightarrow> 
15634  272 
<xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)" 
273 
apply (erule gen_prefix.induct, blast) 

274 
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 

275 
apply (simp_all add: length_type) 

276 
(* Append case is hardest *) 

277 
apply (frule gen_prefix_length_le [THEN le_iff [THEN iffD1]]) 

278 
apply (frule gen_prefix.dom_subset [THEN subsetD], clarify) 

279 
apply (subgoal_tac "length (xs) :nat&length (ys) :nat &length (zs) :nat") 

280 
prefer 2 apply (blast intro: length_type, clarify) 

281 
apply (simp_all add: nth_append length_type length_app) 

282 
apply (rule conjI) 

283 
apply (blast intro: gen_prefix.append) 

46823  284 
apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>?u" in thin_rl) 
15634  285 
apply (erule_tac a = zs in list.cases, auto) 
286 
apply (rule_tac P1 = "%x. <?u (x), ?v>:?w" in nat_diff_split [THEN iffD2]) 

287 
apply auto 

288 
apply (simplesubst append_cons_conv) 

289 
apply (rule_tac [2] gen_prefix.append) 

290 
apply (auto elim: ConsE simp add: gen_prefix_append_both) 

24892  291 
done 
15634  292 

24892  293 
lemma append_one_gen_prefix: "[ <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) ] 
15634  294 
==> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)" 
295 
apply (blast intro: append_one_gen_prefix_lemma) 

296 
done 

297 

298 

299 
(** Proving the equivalence with Charpentier's definition **) 

300 

24892  301 
lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==> 
302 
\<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs) 

46823  303 
\<longrightarrow> <xs, ys>: gen_prefix(A, r) \<longrightarrow> <nth(i, xs), nth(i, ys)>:r" 
24892  304 
apply (induct_tac "xs", simp, clarify) 
305 
apply simp 

306 
apply (erule natE, auto) 

15634  307 
done 
308 

24892  309 
lemma gen_prefix_imp_nth: "[ <xs,ys> \<in> gen_prefix(A,r); i < length(xs)] 
15634  310 
==> <nth(i, xs), nth(i, ys)>:r" 
311 
apply (cut_tac A = A in gen_prefix.dom_subset) 

312 
apply (rule gen_prefix_imp_nth_lemma) 

313 
apply (auto simp add: lt_nat_in_nat) 

314 
done 

315 

24892  316 
lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==> 
317 
\<forall>ys \<in> list(A). length(xs) \<le> length(ys) 

46823  318 
\<longrightarrow> (\<forall>i. i < length(xs) \<longrightarrow> <nth(i, xs), nth(i,ys)>:r) 
319 
\<longrightarrow> <xs, ys> \<in> gen_prefix(A, r)" 

15634  320 
apply (induct_tac "xs") 
321 
apply (simp_all (no_asm_simp)) 

322 
apply clarify 

323 
apply (erule_tac a = ys in list.cases, simp) 

324 
apply (force intro!: nat_0_le simp add: lt_nat_in_nat) 

325 
done 

326 

46823  327 
lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) \<longleftrightarrow> 
24892  328 
(xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) & 
46823  329 
(\<forall>i. i < length(xs) \<longrightarrow> <nth(i,xs), nth(i, ys)>: r))" 
15634  330 
apply (rule iffI) 
331 
apply (frule gen_prefix.dom_subset [THEN subsetD]) 

24892  332 
apply (frule gen_prefix_length_le, auto) 
15634  333 
apply (rule_tac [2] nth_imp_gen_prefix) 
334 
apply (drule gen_prefix_imp_nth) 

335 
apply (auto simp add: lt_nat_in_nat) 

336 
done 

337 

338 
(** prefix is a partial order: **) 

339 

340 
lemma refl_prefix: "refl(list(A), prefix(A))" 

341 
apply (unfold prefix_def) 

342 
apply (rule refl_gen_prefix) 

343 
apply (auto simp add: refl_def) 

344 
done 

345 
declare refl_prefix [THEN reflD, simp] 

346 

347 
lemma trans_prefix: "trans(prefix(A))" 

348 
apply (unfold prefix_def) 

349 
apply (rule trans_gen_prefix) 

350 
apply (auto simp add: trans_def) 

351 
done 

352 

45602  353 
lemmas prefix_trans = trans_prefix [THEN transD] 
15634  354 

355 
lemma trans_on_prefix: "trans[list(A)](prefix(A))" 

356 
apply (unfold prefix_def) 

357 
apply (rule trans_on_gen_prefix) 

358 
apply (auto simp add: trans_def) 

359 
done 

360 

45602  361 
lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD] 
15634  362 

363 
(* Monotonicity of "set" operator WRT prefix *) 

364 

24892  365 
lemma set_of_list_prefix_mono: 
46823  366 
"<xs,ys> \<in> prefix(A) ==> set_of_list(xs) \<subseteq> set_of_list(ys)" 
15634  367 

368 
apply (unfold prefix_def) 

369 
apply (erule gen_prefix.induct) 

370 
apply (subgoal_tac [3] "xs \<in> list (A) &ys \<in> list (A) ") 

371 
prefer 4 apply (blast dest: gen_prefix.dom_subset [THEN subsetD]) 

372 
apply (auto simp add: set_of_list_append) 

373 
done 

374 

375 
(** recursion equations **) 

376 

377 
lemma Nil_prefix: "xs \<in> list(A) ==> <[],xs> \<in> prefix(A)" 

378 

379 
apply (unfold prefix_def) 

380 
apply (simp (no_asm_simp) add: Nil_gen_prefix) 

381 
done 

382 
declare Nil_prefix [simp] 

383 

384 

46823  385 
lemma prefix_Nil: "<xs, []> \<in> prefix(A) \<longleftrightarrow> (xs = [])" 
15634  386 

387 
apply (unfold prefix_def, auto) 

388 
apply (frule gen_prefix.dom_subset [THEN subsetD]) 

389 
apply (drule_tac psi = "<xs, []> \<in> gen_prefix (A, id (A))" in asm_rl) 

390 
apply (simp add: gen_prefix_Nil) 

391 
done 

392 
declare prefix_Nil [iff] 

393 

24892  394 
lemma Cons_prefix_Cons: 
46823  395 
"<Cons(x,xs), Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow> (x=y & <xs,ys> \<in> prefix(A) & y \<in> A)" 
15634  396 
apply (unfold prefix_def, auto) 
397 
done 

398 
declare Cons_prefix_Cons [iff] 

399 

24892  400 
lemma same_prefix_prefix: 
46823  401 
"xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) \<longleftrightarrow> (<ys,zs> \<in> prefix(A))" 
15634  402 
apply (unfold prefix_def) 
403 
apply (subgoal_tac "refl (A,id (A))") 

404 
apply (simp (no_asm_simp)) 

405 
apply (auto simp add: refl_def) 

406 
done 

407 
declare same_prefix_prefix [simp] 

408 

46823  409 
lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))" 
410 
apply (rule_tac P = "%x. <?u, x>:?v \<longleftrightarrow> ?w (x) " in app_right_Nil [THEN subst]) 

15634  411 
apply (rule_tac [2] same_prefix_prefix, auto) 
412 
done 

413 
declare same_prefix_prefix_Nil [simp] 

414 

24892  415 
lemma prefix_appendI: 
15634  416 
"[ <xs,ys> \<in> prefix(A); zs \<in> list(A) ] ==> <xs,ys@zs> \<in> prefix(A)" 
417 
apply (unfold prefix_def) 

418 
apply (erule gen_prefix.append, assumption) 

419 
done 

420 
declare prefix_appendI [simp] 

421 

24892  422 
lemma prefix_Cons: 
423 
"[ xs \<in> list(A); ys \<in> list(A); y \<in> A ] ==> 

46823  424 
<xs,Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow> 
15634  425 
(xs=[]  (\<exists>zs. xs=Cons(y,zs) & <zs,ys> \<in> prefix(A)))" 
426 
apply (unfold prefix_def) 

427 
apply (auto simp add: gen_prefix_Cons) 

428 
done 

429 

24892  430 
lemma append_one_prefix: 
431 
"[ <xs,ys> \<in> prefix(A); length(xs) < length(ys) ] 

15634  432 
==> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)" 
433 
apply (unfold prefix_def) 

434 
apply (subgoal_tac "refl (A, id (A))") 

435 
apply (simp (no_asm_simp) add: append_one_gen_prefix) 

436 
apply (auto simp add: refl_def) 

437 
done 

438 

24892  439 
lemma prefix_length_le: 
15634  440 
"<xs,ys> \<in> prefix(A) ==> length(xs) \<le> length(ys)" 
441 
apply (unfold prefix_def) 

442 
apply (blast dest: gen_prefix_length_le) 

443 
done 

444 

445 
lemma prefix_type: "prefix(A)<=list(A)*list(A)" 

446 
apply (unfold prefix_def) 

447 
apply (blast intro!: gen_prefix.dom_subset) 

448 
done 

449 

24892  450 
lemma strict_prefix_type: 
46823  451 
"strict_prefix(A) \<subseteq> list(A)*list(A)" 
15634  452 
apply (unfold strict_prefix_def) 
453 
apply (blast intro!: prefix_type [THEN subsetD]) 

454 
done 

455 

24892  456 
lemma strict_prefix_length_lt_aux: 
46823  457 
"<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys \<longrightarrow> length(xs) < length(ys)" 
15634  458 
apply (unfold prefix_def) 
459 
apply (erule gen_prefix.induct, clarify) 

460 
apply (subgoal_tac [!] "ys \<in> list(A) & xs \<in> list(A)") 

461 
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] 

462 
simp add: length_type) 

463 
apply (subgoal_tac "length (zs) =0") 

464 
apply (drule_tac [2] not_lt_imp_le) 

465 
apply (rule_tac [5] j = "length (ys) " in lt_trans2) 

466 
apply auto 

467 
done 

468 

24892  469 
lemma strict_prefix_length_lt: 
15634  470 
"<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)" 
471 
apply (unfold strict_prefix_def) 

472 
apply (rule strict_prefix_length_lt_aux [THEN mp]) 

473 
apply (auto dest: prefix_type [THEN subsetD]) 

474 
done 

475 

476 
(*Equivalence to the definition used in Lex/Prefix.thy*) 

24892  477 
lemma prefix_iff: 
46823  478 
"<xs,zs> \<in> prefix(A) \<longleftrightarrow> (\<exists>ys \<in> list(A). zs = xs@ys) & xs \<in> list(A)" 
15634  479 
apply (unfold prefix_def) 
480 
apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app) 

481 
apply (subgoal_tac "drop (length (xs), zs) \<in> list (A) ") 

482 
apply (rule_tac x = "drop (length (xs), zs) " in bexI) 

483 
apply safe 

484 
prefer 2 apply (simp add: length_type drop_type) 

485 
apply (rule nth_equalityI) 

486 
apply (simp_all (no_asm_simp) add: nth_append app_type drop_type length_app length_drop) 

487 
apply (rule nat_diff_split [THEN iffD2], simp_all, clarify) 

488 
apply (drule_tac i = "length (zs) " in leI) 

489 
apply (force simp add: le_subset_iff, safe) 

490 
apply (subgoal_tac "length (xs) #+ (i # length (xs)) = i") 

491 
apply (subst nth_drop) 

492 
apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split) 

493 
done 

494 

24892  495 
lemma prefix_snoc: 
496 
"[xs \<in> list(A); ys \<in> list(A); y \<in> A ] ==> 

46823  497 
<xs, ys@[y]> \<in> prefix(A) \<longleftrightarrow> (xs = ys@[y]  <xs,ys> \<in> prefix(A))" 
15634  498 
apply (simp (no_asm) add: prefix_iff) 
499 
apply (rule iffI, clarify) 

500 
apply (erule_tac xs = ysa in rev_list_elim, simp) 

501 
apply (simp add: app_type app_assoc [symmetric]) 

502 
apply (auto simp add: app_assoc app_type) 

503 
done 

504 
declare prefix_snoc [simp] 

505 

24892  506 
lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A). 
46823  507 
(<xs, ys@zs> \<in> prefix(A)) \<longleftrightarrow> 
15634  508 
(<xs,ys> \<in> prefix(A)  (\<exists>us. xs = ys@us & <us,zs> \<in> prefix(A)))" 
24892  509 
apply (erule list_append_induct, force, clarify) 
510 
apply (rule iffI) 

15634  511 
apply (simp add: add: app_assoc [symmetric]) 
24892  512 
apply (erule disjE) 
513 
apply (rule disjI2) 

514 
apply (rule_tac x = "y @ [x]" in exI) 

15634  515 
apply (simp add: add: app_assoc [symmetric], force+) 
516 
done 

517 

518 

519 
(*Although the prefix ordering is not linear, the prefixes of a list 

520 
are linearly ordered.*) 

24892  521 
lemma common_prefix_linear_lemma [rule_format]: "[ zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) ] 
46823  522 
==> <xs, zs> \<in> prefix(A) \<longrightarrow> <ys,zs> \<in> prefix(A) 
523 
\<longrightarrow><xs,ys> \<in> prefix(A)  <ys,xs> \<in> prefix(A)" 

15634  524 
apply (erule list_append_induct, auto) 
525 
done 

526 

24892  527 
lemma common_prefix_linear: "[<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) ] 
15634  528 
==> <xs,ys> \<in> prefix(A)  <ys,xs> \<in> prefix(A)" 
529 
apply (cut_tac prefix_type) 

530 
apply (blast del: disjCI intro: common_prefix_linear_lemma) 

531 
done 

532 

533 

534 
(*** pfixLe, pfixGe \<in> properties inherited from the translations ***) 

535 

536 

537 

538 
(** pfixLe **) 

539 

540 
lemma refl_Le: "refl(nat,Le)" 

541 

542 
apply (unfold refl_def, auto) 

543 
done 

544 
declare refl_Le [simp] 

545 

546 
lemma antisym_Le: "antisym(Le)" 

547 
apply (unfold antisym_def) 

548 
apply (auto intro: le_anti_sym) 

549 
done 

550 
declare antisym_Le [simp] 

551 

552 
lemma trans_on_Le: "trans[nat](Le)" 

553 
apply (unfold trans_on_def, auto) 

554 
apply (blast intro: le_trans) 

555 
done 

556 
declare trans_on_Le [simp] 

557 

558 
lemma trans_Le: "trans(Le)" 

559 
apply (unfold trans_def, auto) 

560 
apply (blast intro: le_trans) 

561 
done 

562 
declare trans_Le [simp] 

563 

564 
lemma part_order_Le: "part_order(nat,Le)" 

565 
by (unfold part_order_def, auto) 

566 
declare part_order_Le [simp] 

567 

568 
lemma pfixLe_refl: "x \<in> list(nat) ==> x pfixLe x" 

569 
by (blast intro: refl_gen_prefix [THEN reflD] refl_Le) 

570 
declare pfixLe_refl [simp] 

571 

572 
lemma pfixLe_trans: "[ x pfixLe y; y pfixLe z ] ==> x pfixLe z" 

573 
by (blast intro: trans_gen_prefix [THEN transD] trans_Le) 

574 

575 
lemma pfixLe_antisym: "[ x pfixLe y; y pfixLe x ] ==> x = y" 

576 
by (blast intro: antisym_gen_prefix [THEN antisymE] antisym_Le) 

577 

578 

24892  579 
lemma prefix_imp_pfixLe: 
15634  580 
"<xs,ys>:prefix(nat)==> xs pfixLe ys" 
581 

582 
apply (unfold prefix_def) 

583 
apply (rule gen_prefix_mono [THEN subsetD], auto) 

584 
done 

585 

586 
lemma refl_Ge: "refl(nat, Ge)" 

587 
by (unfold refl_def Ge_def, auto) 

588 
declare refl_Ge [iff] 

589 

590 
lemma antisym_Ge: "antisym(Ge)" 

591 
apply (unfold antisym_def Ge_def) 

592 
apply (auto intro: le_anti_sym) 

593 
done 

594 
declare antisym_Ge [iff] 

595 

596 
lemma trans_Ge: "trans(Ge)" 

597 
apply (unfold trans_def Ge_def) 

598 
apply (auto intro: le_trans) 

599 
done 

600 
declare trans_Ge [iff] 

601 

602 
lemma pfixGe_refl: "x \<in> list(nat) ==> x pfixGe x" 

603 
by (blast intro: refl_gen_prefix [THEN reflD]) 

604 
declare pfixGe_refl [simp] 

605 

606 
lemma pfixGe_trans: "[ x pfixGe y; y pfixGe z ] ==> x pfixGe z" 

607 
by (blast intro: trans_gen_prefix [THEN transD]) 

608 

609 
lemma pfixGe_antisym: "[ x pfixGe y; y pfixGe x ] ==> x = y" 

610 
by (blast intro: antisym_gen_prefix [THEN antisymE]) 

611 

24892  612 
lemma prefix_imp_pfixGe: 
15634  613 
"<xs,ys>:prefix(nat) ==> xs pfixGe ys" 
614 
apply (unfold prefix_def Ge_def) 

615 
apply (rule gen_prefix_mono [THEN subsetD], auto) 

616 
done 

617 
(* Added by Sidi \<in> prefix and take *) 

618 

24892  619 
lemma prefix_imp_take: 
15634  620 
"<xs, ys> \<in> prefix(A) ==> xs = take(length(xs), ys)" 
621 

622 
apply (unfold prefix_def) 

623 
apply (erule gen_prefix.induct) 

624 
apply (subgoal_tac [3] "length (xs) :nat") 

625 
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: length_type) 

626 
apply (frule gen_prefix.dom_subset [THEN subsetD]) 

627 
apply (frule gen_prefix_length_le) 

628 
apply (auto simp add: take_append) 

629 
apply (subgoal_tac "length (xs) # length (ys) =0") 

630 
apply (simp_all (no_asm_simp) add: diff_is_0_iff) 

631 
done 

632 

633 
lemma prefix_length_equal: "[<xs,ys> \<in> prefix(A); length(xs)=length(ys)] ==> xs = ys" 

634 
apply (cut_tac A = A in prefix_type) 

635 
apply (drule subsetD, auto) 

636 
apply (drule prefix_imp_take) 

637 
apply (erule trans, simp) 

638 
done 

639 

640 
lemma prefix_length_le_equal: "[<xs,ys> \<in> prefix(A); length(ys) \<le> length(xs)] ==> xs = ys" 

641 
by (blast intro: prefix_length_equal le_anti_sym prefix_length_le) 

642 

643 
lemma take_prefix [rule_format]: "xs \<in> list(A) ==> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)" 

644 
apply (unfold prefix_def) 

645 
apply (erule list.induct, simp, clarify) 

646 
apply (erule natE, auto) 

647 
done 

648 

46823  649 
lemma prefix_take_iff: "<xs,ys> \<in> prefix(A) \<longleftrightarrow> (xs=take(length(xs), ys) & xs \<in> list(A) & ys \<in> list(A))" 
15634  650 
apply (rule iffI) 
651 
apply (frule prefix_type [THEN subsetD]) 

652 
apply (blast intro: prefix_imp_take, clarify) 

653 
apply (erule ssubst) 

654 
apply (blast intro: take_prefix length_type) 

655 
done 

656 

657 
lemma prefix_imp_nth: "[ <xs,ys> \<in> prefix(A); i < length(xs)] ==> nth(i,xs) = nth(i,ys)" 

658 
by (auto dest!: gen_prefix_imp_nth simp add: prefix_def) 

659 

24892  660 
lemma nth_imp_prefix: 
661 
"[xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys); 

662 
!!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)] 

15634  663 
==> <xs,ys> \<in> prefix(A)" 
664 
apply (auto simp add: prefix_def nth_imp_gen_prefix) 

665 
apply (auto intro!: nth_imp_gen_prefix simp add: prefix_def) 

666 
apply (blast intro: nth_type lt_trans2) 

667 
done 

668 

669 

24892  670 
lemma length_le_prefix_imp_prefix: "[length(xs) \<le> length(ys); 
15634  671 
<xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)] ==> <xs,ys> \<in> prefix(A)" 
672 
apply (cut_tac A = A in prefix_type) 

673 
apply (rule nth_imp_prefix, blast, blast) 

674 
apply assumption 

675 
apply (rule_tac b = "nth (i,zs)" in trans) 

676 
apply (blast intro: prefix_imp_nth) 

677 
apply (blast intro: sym prefix_imp_nth prefix_length_le lt_trans2) 

678 
done 

679 

12197  680 
end 