15634
|
1 |
(* ID: $Id$
|
12197
|
2 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
|
|
3 |
Copyright 2001 University of Cambridge
|
|
4 |
|
|
5 |
<xs,ys>:gen_prefix(r)
|
|
6 |
if ys = xs' @ zs where length(xs) = length(xs')
|
|
7 |
and corresponding elements of xs, xs' are pairwise related by r
|
|
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 |
|
12197
|
28 |
domains "gen_prefix(A, r)" <= "list(A)*list(A)"
|
24892
|
29 |
|
15634
|
30 |
intros
|
|
31 |
Nil: "<[],[]>:gen_prefix(A, r)"
|
12197
|
32 |
|
15634
|
33 |
prepend: "[| <xs,ys>:gen_prefix(A, r); <x,y>:r; x:A; y:A |]
|
12197
|
34 |
==> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)"
|
|
35 |
|
15634
|
36 |
append: "[| <xs,ys>:gen_prefix(A, r); zs:list(A) |]
|
|
37 |
==> <xs, ys@zs>:gen_prefix(A, r)"
|
|
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) |]
|
|
82 |
==> (\<forall>x xs. x \<in> A --> xs'= Cons(x,xs) -->
|
|
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))
|
15634
|
100 |
<-> (x \<in> A & y \<in> A & <x,y>:r & <xs,ys> \<in> gen_prefix(A, r))"
|
|
101 |
apply (auto intro: gen_prefix.prepend)
|
|
102 |
done
|
|
103 |
declare Cons_gen_prefix_Cons [iff]
|
|
104 |
|
|
105 |
(** Monotonicity of gen_prefix **)
|
|
106 |
|
|
107 |
lemma gen_prefix_mono2: "r<=s ==> gen_prefix(A, r) <= gen_prefix(A, s)"
|
|
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 |
|
|
115 |
lemma gen_prefix_mono1: "A<=B ==>gen_prefix(A, r) <= gen_prefix(B, r)"
|
|
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 |
|
|
129 |
lemma gen_prefix_mono: "[| A <= B; r <= s |] ==> gen_prefix(A, r) <= gen_prefix(B, s)"
|
|
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) ==>
|
15634
|
148 |
\<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)"
|
|
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) ==>
|
15634
|
157 |
(\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)--><x, z> \<in> gen_prefix(A, s O r))"
|
|
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 |
|
|
165 |
lemma trans_comp_subset: "trans(r) ==> r O r <= r"
|
|
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 |
|
|
201 |
lemma nat_le_lemma [rule_format]: "n \<in> nat ==> \<forall>b \<in> nat. n #+ b \<le> n --> b = 0"
|
|
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 |
|
|
228 |
lemma gen_prefix_Nil: "xs \<in> list(A) ==> <xs, []> \<in> gen_prefix(A,r) <-> (xs = [])"
|
|
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) |] ==>
|
15634
|
234 |
<xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs> \<in> gen_prefix(A, r)"
|
|
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 |] ==>
|
|
242 |
<xs, Cons(y,ys)> \<in> gen_prefix(A,r) <->
|
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) |]
|
|
271 |
==> length(xs) < length(ys) -->
|
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)
|
|
284 |
apply (erule_tac V = "length (xs) < length (ys) -->?u" in thin_rl)
|
|
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)
|
15634
|
303 |
--> <xs, ys>: gen_prefix(A, r) --> <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)
|
|
318 |
--> (\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r)
|
15634
|
319 |
--> <xs, ys> \<in> gen_prefix(A, r)"
|
|
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 |
|
24892
|
327 |
lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) <->
|
|
328 |
(xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) &
|
15634
|
329 |
(\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))"
|
|
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 |
|
|
353 |
lemmas prefix_trans = trans_prefix [THEN transD, standard]
|
|
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 |
|
|
361 |
lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD, standard]
|
|
362 |
|
|
363 |
(* Monotonicity of "set" operator WRT prefix *)
|
|
364 |
|
24892
|
365 |
lemma set_of_list_prefix_mono:
|
15634
|
366 |
"<xs,ys> \<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)"
|
|
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 |
|
|
385 |
lemma prefix_Nil: "<xs, []> \<in> prefix(A) <-> (xs = [])"
|
|
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:
|
15634
|
395 |
"<Cons(x,xs), Cons(y,ys)> \<in> prefix(A) <-> (x=y & <xs,ys> \<in> prefix(A) & y \<in> A)"
|
|
396 |
apply (unfold prefix_def, auto)
|
|
397 |
done
|
|
398 |
declare Cons_prefix_Cons [iff]
|
|
399 |
|
24892
|
400 |
lemma same_prefix_prefix:
|
15634
|
401 |
"xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) <-> (<ys,zs> \<in> prefix(A))"
|
|
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 |
|
|
409 |
lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) <-> (<ys,[]> \<in> prefix(A))"
|
|
410 |
apply (rule_tac P = "%x. <?u, x>:?v <-> ?w (x) " in app_right_Nil [THEN subst])
|
|
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 |] ==>
|
|
424 |
<xs,Cons(y,ys)> \<in> prefix(A) <->
|
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:
|
15634
|
451 |
"strict_prefix(A) <= list(A)*list(A)"
|
|
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:
|
15634
|
457 |
"<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys --> length(xs) < length(ys)"
|
|
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:
|
15634
|
478 |
"<xs,zs> \<in> prefix(A) <-> (\<exists>ys \<in> list(A). zs = xs@ys) & xs \<in> list(A)"
|
|
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 |] ==>
|
15634
|
497 |
<xs, ys@[y]> \<in> prefix(A) <-> (xs = ys@[y] | <xs,ys> \<in> prefix(A))"
|
|
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).
|
|
507 |
(<xs, ys@zs> \<in> prefix(A)) <->
|
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) |]
|
|
522 |
==> <xs, zs> \<in> prefix(A) --> <ys,zs> \<in> prefix(A)
|
15634
|
523 |
--><xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
|
|
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 |
|
|
649 |
lemma prefix_take_iff: "<xs,ys> \<in> prefix(A) <-> (xs=take(length(xs), ys) & xs \<in> list(A) & ys \<in> list(A))"
|
|
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
|