|
1 |
|
2 theory PositionsExt |
|
3 imports "SpecExt" "LexerExt" |
|
4 begin |
|
5 |
|
6 section {* Positions in Values *} |
|
7 |
|
8 fun |
|
9 at :: "val \<Rightarrow> nat list \<Rightarrow> val" |
|
10 where |
|
11 "at v [] = v" |
|
12 | "at (Left v) (0#ps)= at v ps" |
|
13 | "at (Right v) (Suc 0#ps)= at v ps" |
|
14 | "at (Seq v1 v2) (0#ps)= at v1 ps" |
|
15 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps" |
|
16 | "at (Stars vs) (n#ps)= at (nth vs n) ps" |
|
17 |
|
18 |
|
19 |
|
20 fun Pos :: "val \<Rightarrow> (nat list) set" |
|
21 where |
|
22 "Pos (Void) = {[]}" |
|
23 | "Pos (Char c) = {[]}" |
|
24 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}" |
|
25 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}" |
|
26 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" |
|
27 | "Pos (Stars []) = {[]}" |
|
28 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}" |
|
29 |
|
30 |
|
31 lemma Pos_stars: |
|
32 "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})" |
|
33 apply(induct vs) |
|
34 apply(auto simp add: insert_ident less_Suc_eq_0_disj) |
|
35 done |
|
36 |
|
37 lemma Pos_empty: |
|
38 shows "[] \<in> Pos v" |
|
39 by (induct v rule: Pos.induct)(auto) |
|
40 |
|
41 |
|
42 abbreviation |
|
43 "intlen vs \<equiv> int (length vs)" |
|
44 |
|
45 |
|
46 definition pflat_len :: "val \<Rightarrow> nat list => int" |
|
47 where |
|
48 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
|
49 |
|
50 lemma pflat_len_simps: |
|
51 shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p" |
|
52 and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p" |
|
53 and "pflat_len (Left v) (0#p) = pflat_len v p" |
|
54 and "pflat_len (Left v) (Suc 0#p) = -1" |
|
55 and "pflat_len (Right v) (Suc 0#p) = pflat_len v p" |
|
56 and "pflat_len (Right v) (0#p) = -1" |
|
57 and "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)" |
|
58 and "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p" |
|
59 and "pflat_len v [] = intlen (flat v)" |
|
60 by (auto simp add: pflat_len_def Pos_empty) |
|
61 |
|
62 lemma pflat_len_Stars_simps: |
|
63 assumes "n < length vs" |
|
64 shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p" |
|
65 using assms |
|
66 apply(induct vs arbitrary: n p) |
|
67 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps) |
|
68 done |
|
69 |
|
70 lemma pflat_len_outside: |
|
71 assumes "p \<notin> Pos v1" |
|
72 shows "pflat_len v1 p = -1 " |
|
73 using assms by (simp add: pflat_len_def) |
|
74 |
|
75 |
|
76 |
|
77 section {* Orderings *} |
|
78 |
|
79 |
|
80 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60) |
|
81 where |
|
82 "ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2" |
|
83 |
|
84 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60) |
|
85 where |
|
86 "ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2" |
|
87 |
|
88 inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60) |
|
89 where |
|
90 "[] \<sqsubset>lex (p#ps)" |
|
91 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)" |
|
92 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)" |
|
93 |
|
94 lemma lex_irrfl: |
|
95 fixes ps1 ps2 :: "nat list" |
|
96 assumes "ps1 \<sqsubset>lex ps2" |
|
97 shows "ps1 \<noteq> ps2" |
|
98 using assms |
|
99 by(induct rule: lex_list.induct)(auto) |
|
100 |
|
101 lemma lex_simps [simp]: |
|
102 fixes xs ys :: "nat list" |
|
103 shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []" |
|
104 and "xs \<sqsubset>lex [] \<longleftrightarrow> False" |
|
105 and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))" |
|
106 by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros) |
|
107 |
|
108 lemma lex_trans: |
|
109 fixes ps1 ps2 ps3 :: "nat list" |
|
110 assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3" |
|
111 shows "ps1 \<sqsubset>lex ps3" |
|
112 using assms |
|
113 by (induct arbitrary: ps3 rule: lex_list.induct) |
|
114 (auto elim: lex_list.cases) |
|
115 |
|
116 |
|
117 lemma lex_trichotomous: |
|
118 fixes p q :: "nat list" |
|
119 shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p" |
|
120 apply(induct p arbitrary: q) |
|
121 apply(auto elim: lex_list.cases) |
|
122 apply(case_tac q) |
|
123 apply(auto) |
|
124 done |
|
125 |
|
126 |
|
127 |
|
128 |
|
129 section {* POSIX Ordering of Values According to Okui & Suzuki *} |
|
130 |
|
131 |
|
132 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60) |
|
133 where |
|
134 "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and> |
|
135 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
|
136 |
|
137 lemma PosOrd_def2: |
|
138 shows "v1 \<sqsubset>val p v2 \<longleftrightarrow> |
|
139 pflat_len v1 p > pflat_len v2 p \<and> |
|
140 (\<forall>q \<in> Pos v1. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q) \<and> |
|
141 (\<forall>q \<in> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)" |
|
142 unfolding PosOrd_def |
|
143 apply(auto) |
|
144 done |
|
145 |
|
146 |
|
147 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60) |
|
148 where |
|
149 "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2" |
|
150 |
|
151 definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60) |
|
152 where |
|
153 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
|
154 |
|
155 |
|
156 lemma PosOrd_trans: |
|
157 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
|
158 shows "v1 :\<sqsubset>val v3" |
|
159 proof - |
|
160 from assms obtain p p' |
|
161 where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast |
|
162 then have pos: "p \<in> Pos v1" "p' \<in> Pos v2" unfolding PosOrd_def pflat_len_def |
|
163 by (smt not_int_zless_negative)+ |
|
164 have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p" |
|
165 by (rule lex_trichotomous) |
|
166 moreover |
|
167 { assume "p = p'" |
|
168 with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def |
|
169 by (smt Un_iff) |
|
170 then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
171 } |
|
172 moreover |
|
173 { assume "p \<sqsubset>lex p'" |
|
174 with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def |
|
175 by (smt Un_iff lex_trans) |
|
176 then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
177 } |
|
178 moreover |
|
179 { assume "p' \<sqsubset>lex p" |
|
180 with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def |
|
181 by (smt Un_iff lex_trans pflat_len_def) |
|
182 then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast |
|
183 } |
|
184 ultimately show "v1 :\<sqsubset>val v3" by blast |
|
185 qed |
|
186 |
|
187 lemma PosOrd_irrefl: |
|
188 assumes "v :\<sqsubset>val v" |
|
189 shows "False" |
|
190 using assms unfolding PosOrd_ex_def PosOrd_def |
|
191 by auto |
|
192 |
|
193 lemma PosOrd_assym: |
|
194 assumes "v1 :\<sqsubset>val v2" |
|
195 shows "\<not>(v2 :\<sqsubset>val v1)" |
|
196 using assms |
|
197 using PosOrd_irrefl PosOrd_trans by blast |
|
198 |
|
199 text {* |
|
200 :\<sqsubseteq>val and :\<sqsubset>val are partial orders. |
|
201 *} |
|
202 |
|
203 lemma PosOrd_ordering: |
|
204 shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
|
205 unfolding ordering_def PosOrd_ex_eq_def |
|
206 apply(auto) |
|
207 using PosOrd_irrefl apply blast |
|
208 using PosOrd_assym apply blast |
|
209 using PosOrd_trans by blast |
|
210 |
|
211 lemma PosOrd_order: |
|
212 shows "class.order (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)" |
|
213 using PosOrd_ordering |
|
214 apply(simp add: class.order_def class.preorder_def class.order_axioms_def) |
|
215 unfolding ordering_def |
|
216 by blast |
|
217 |
|
218 |
|
219 lemma PosOrd_ex_eq2: |
|
220 shows "v1 :\<sqsubset>val v2 \<longleftrightarrow> (v1 :\<sqsubseteq>val v2 \<and> v1 \<noteq> v2)" |
|
221 using PosOrd_ordering |
|
222 unfolding ordering_def |
|
223 by auto |
|
224 |
|
225 lemma PosOrdeq_trans: |
|
226 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v3" |
|
227 shows "v1 :\<sqsubseteq>val v3" |
|
228 using assms PosOrd_ordering |
|
229 unfolding ordering_def |
|
230 by blast |
|
231 |
|
232 lemma PosOrdeq_antisym: |
|
233 assumes "v1 :\<sqsubseteq>val v2" "v2 :\<sqsubseteq>val v1" |
|
234 shows "v1 = v2" |
|
235 using assms PosOrd_ordering |
|
236 unfolding ordering_def |
|
237 by blast |
|
238 |
|
239 lemma PosOrdeq_refl: |
|
240 shows "v :\<sqsubseteq>val v" |
|
241 unfolding PosOrd_ex_eq_def |
|
242 by auto |
|
243 |
|
244 |
|
245 lemma PosOrd_shorterE: |
|
246 assumes "v1 :\<sqsubset>val v2" |
|
247 shows "length (flat v2) \<le> length (flat v1)" |
|
248 using assms unfolding PosOrd_ex_def PosOrd_def |
|
249 apply(auto) |
|
250 apply(case_tac p) |
|
251 apply(simp add: pflat_len_simps) |
|
252 apply(drule_tac x="[]" in bspec) |
|
253 apply(simp add: Pos_empty) |
|
254 apply(simp add: pflat_len_simps) |
|
255 done |
|
256 |
|
257 lemma PosOrd_shorterI: |
|
258 assumes "length (flat v2) < length (flat v1)" |
|
259 shows "v1 :\<sqsubset>val v2" |
|
260 unfolding PosOrd_ex_def PosOrd_def pflat_len_def |
|
261 using assms Pos_empty by force |
|
262 |
|
263 lemma PosOrd_spreI: |
|
264 assumes "flat v' \<sqsubset>spre flat v" |
|
265 shows "v :\<sqsubset>val v'" |
|
266 using assms |
|
267 apply(rule_tac PosOrd_shorterI) |
|
268 unfolding prefix_list_def sprefix_list_def |
|
269 by (metis append_Nil2 append_eq_conv_conj drop_all le_less_linear) |
|
270 |
|
271 lemma pflat_len_inside: |
|
272 assumes "pflat_len v2 p < pflat_len v1 p" |
|
273 shows "p \<in> Pos v1" |
|
274 using assms |
|
275 unfolding pflat_len_def |
|
276 by (auto split: if_splits) |
|
277 |
|
278 |
|
279 lemma PosOrd_Left_Right: |
|
280 assumes "flat v1 = flat v2" |
|
281 shows "Left v1 :\<sqsubset>val Right v2" |
|
282 unfolding PosOrd_ex_def |
|
283 apply(rule_tac x="[0]" in exI) |
|
284 apply(auto simp add: PosOrd_def pflat_len_simps assms) |
|
285 done |
|
286 |
|
287 lemma PosOrd_LeftE: |
|
288 assumes "Left v1 :\<sqsubset>val Left v2" "flat v1 = flat v2" |
|
289 shows "v1 :\<sqsubset>val v2" |
|
290 using assms |
|
291 unfolding PosOrd_ex_def PosOrd_def2 |
|
292 apply(auto simp add: pflat_len_simps) |
|
293 apply(frule pflat_len_inside) |
|
294 apply(auto simp add: pflat_len_simps) |
|
295 by (metis lex_simps(3) pflat_len_simps(3)) |
|
296 |
|
297 lemma PosOrd_LeftI: |
|
298 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
|
299 shows "Left v1 :\<sqsubset>val Left v2" |
|
300 using assms |
|
301 unfolding PosOrd_ex_def PosOrd_def2 |
|
302 apply(auto simp add: pflat_len_simps) |
|
303 by (metis less_numeral_extra(3) lex_simps(3) pflat_len_simps(3)) |
|
304 |
|
305 lemma PosOrd_Left_eq: |
|
306 assumes "flat v1 = flat v2" |
|
307 shows "Left v1 :\<sqsubset>val Left v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" |
|
308 using assms PosOrd_LeftE PosOrd_LeftI |
|
309 by blast |
|
310 |
|
311 |
|
312 lemma PosOrd_RightE: |
|
313 assumes "Right v1 :\<sqsubset>val Right v2" "flat v1 = flat v2" |
|
314 shows "v1 :\<sqsubset>val v2" |
|
315 using assms |
|
316 unfolding PosOrd_ex_def PosOrd_def2 |
|
317 apply(auto simp add: pflat_len_simps) |
|
318 apply(frule pflat_len_inside) |
|
319 apply(auto simp add: pflat_len_simps) |
|
320 by (metis lex_simps(3) pflat_len_simps(5)) |
|
321 |
|
322 lemma PosOrd_RightI: |
|
323 assumes "v1 :\<sqsubset>val v2" "flat v1 = flat v2" |
|
324 shows "Right v1 :\<sqsubset>val Right v2" |
|
325 using assms |
|
326 unfolding PosOrd_ex_def PosOrd_def2 |
|
327 apply(auto simp add: pflat_len_simps) |
|
328 by (metis lex_simps(3) nat_neq_iff pflat_len_simps(5)) |
|
329 |
|
330 |
|
331 lemma PosOrd_Right_eq: |
|
332 assumes "flat v1 = flat v2" |
|
333 shows "Right v1 :\<sqsubset>val Right v2 \<longleftrightarrow> v1 :\<sqsubset>val v2" |
|
334 using assms PosOrd_RightE PosOrd_RightI |
|
335 by blast |
|
336 |
|
337 |
|
338 lemma PosOrd_SeqI1: |
|
339 assumes "v1 :\<sqsubset>val w1" "flat (Seq v1 v2) = flat (Seq w1 w2)" |
|
340 shows "Seq v1 v2 :\<sqsubset>val Seq w1 w2" |
|
341 using assms(1) |
|
342 apply(subst (asm) PosOrd_ex_def) |
|
343 apply(subst (asm) PosOrd_def) |
|
344 apply(clarify) |
|
345 apply(subst PosOrd_ex_def) |
|
346 apply(rule_tac x="0#p" in exI) |
|
347 apply(subst PosOrd_def) |
|
348 apply(rule conjI) |
|
349 apply(simp add: pflat_len_simps) |
|
350 apply(rule ballI) |
|
351 apply(rule impI) |
|
352 apply(simp only: Pos.simps) |
|
353 apply(auto)[1] |
|
354 apply(simp add: pflat_len_simps) |
|
355 apply(auto simp add: pflat_len_simps) |
|
356 using assms(2) |
|
357 apply(simp) |
|
358 apply(metis length_append of_nat_add) |
|
359 done |
|
360 |
|
361 lemma PosOrd_SeqI2: |
|
362 assumes "v2 :\<sqsubset>val w2" "flat v2 = flat w2" |
|
363 shows "Seq v v2 :\<sqsubset>val Seq v w2" |
|
364 using assms(1) |
|
365 apply(subst (asm) PosOrd_ex_def) |
|
366 apply(subst (asm) PosOrd_def) |
|
367 apply(clarify) |
|
368 apply(subst PosOrd_ex_def) |
|
369 apply(rule_tac x="Suc 0#p" in exI) |
|
370 apply(subst PosOrd_def) |
|
371 apply(rule conjI) |
|
372 apply(simp add: pflat_len_simps) |
|
373 apply(rule ballI) |
|
374 apply(rule impI) |
|
375 apply(simp only: Pos.simps) |
|
376 apply(auto)[1] |
|
377 apply(simp add: pflat_len_simps) |
|
378 using assms(2) |
|
379 apply(simp) |
|
380 apply(auto simp add: pflat_len_simps) |
|
381 done |
|
382 |
|
383 lemma PosOrd_Seq_eq: |
|
384 assumes "flat v2 = flat w2" |
|
385 shows "(Seq v v2) :\<sqsubset>val (Seq v w2) \<longleftrightarrow> v2 :\<sqsubset>val w2" |
|
386 using assms |
|
387 apply(auto) |
|
388 prefer 2 |
|
389 apply(simp add: PosOrd_SeqI2) |
|
390 apply(simp add: PosOrd_ex_def) |
|
391 apply(auto) |
|
392 apply(case_tac p) |
|
393 apply(simp add: PosOrd_def pflat_len_simps) |
|
394 apply(case_tac a) |
|
395 apply(simp add: PosOrd_def pflat_len_simps) |
|
396 apply(clarify) |
|
397 apply(case_tac nat) |
|
398 prefer 2 |
|
399 apply(simp add: PosOrd_def pflat_len_simps pflat_len_outside) |
|
400 apply(rule_tac x="list" in exI) |
|
401 apply(auto simp add: PosOrd_def2 pflat_len_simps) |
|
402 apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2)) |
|
403 apply(smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(2)) |
|
404 done |
|
405 |
|
406 |
|
407 |
|
408 lemma PosOrd_StarsI: |
|
409 assumes "v1 :\<sqsubset>val v2" "flats (v1#vs1) = flats (v2#vs2)" |
|
410 shows "Stars (v1#vs1) :\<sqsubset>val Stars (v2#vs2)" |
|
411 using assms(1) |
|
412 apply(subst (asm) PosOrd_ex_def) |
|
413 apply(subst (asm) PosOrd_def) |
|
414 apply(clarify) |
|
415 apply(subst PosOrd_ex_def) |
|
416 apply(subst PosOrd_def) |
|
417 apply(rule_tac x="0#p" in exI) |
|
418 apply(simp add: pflat_len_Stars_simps pflat_len_simps) |
|
419 using assms(2) |
|
420 apply(simp add: pflat_len_simps) |
|
421 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps) |
|
422 by (metis length_append of_nat_add) |
|
423 |
|
424 lemma PosOrd_StarsI2: |
|
425 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flats vs1 = flats vs2" |
|
426 shows "Stars (v#vs1) :\<sqsubset>val Stars (v#vs2)" |
|
427 using assms(1) |
|
428 apply(subst (asm) PosOrd_ex_def) |
|
429 apply(subst (asm) PosOrd_def) |
|
430 apply(clarify) |
|
431 apply(subst PosOrd_ex_def) |
|
432 apply(subst PosOrd_def) |
|
433 apply(case_tac p) |
|
434 apply(simp add: pflat_len_simps) |
|
435 apply(rule_tac x="Suc a#list" in exI) |
|
436 apply(auto simp add: pflat_len_Stars_simps pflat_len_simps assms(2)) |
|
437 done |
|
438 |
|
439 lemma PosOrd_Stars_appendI: |
|
440 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
|
441 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
442 using assms |
|
443 apply(induct vs) |
|
444 apply(simp) |
|
445 apply(simp add: PosOrd_StarsI2) |
|
446 done |
|
447 |
|
448 lemma PosOrd_eq_Stars_zipI: |
|
449 assumes "\<forall>(v1, v2) \<in> set (zip vs1 vs2). v1 :\<sqsubseteq>val v2" |
|
450 "length vs1 = length vs2" "flats vs1 = flats vs2" |
|
451 shows "Stars vs1 :\<sqsubseteq>val Stars vs2" |
|
452 using assms |
|
453 apply(induct vs1 arbitrary: vs2) |
|
454 apply(case_tac vs2) |
|
455 apply(simp add: PosOrd_ex_eq_def) |
|
456 apply(simp) |
|
457 apply(case_tac vs2) |
|
458 apply(simp) |
|
459 apply(simp) |
|
460 apply(auto) |
|
461 apply(subst (asm) (2)PosOrd_ex_eq_def) |
|
462 apply(auto) |
|
463 apply(subst PosOrd_ex_eq_def) |
|
464 apply(rule disjI1) |
|
465 apply(rule PosOrd_StarsI) |
|
466 apply(simp) |
|
467 apply(simp) |
|
468 using PosOrd_StarsI2 PosOrd_ex_eq_def by fastforce |
|
469 |
|
470 lemma PosOrd_StarsE2: |
|
471 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
|
472 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
473 using assms |
|
474 apply(subst (asm) PosOrd_ex_def) |
|
475 apply(erule exE) |
|
476 apply(case_tac p) |
|
477 apply(simp) |
|
478 apply(simp add: PosOrd_def pflat_len_simps) |
|
479 apply(subst PosOrd_ex_def) |
|
480 apply(rule_tac x="[]" in exI) |
|
481 apply(simp add: PosOrd_def pflat_len_simps Pos_empty) |
|
482 apply(simp) |
|
483 apply(case_tac a) |
|
484 apply(clarify) |
|
485 apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1] |
|
486 apply(clarify) |
|
487 apply(simp add: PosOrd_ex_def) |
|
488 apply(rule_tac x="nat#list" in exI) |
|
489 apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
|
490 apply(case_tac q) |
|
491 apply(simp add: PosOrd_def pflat_len_simps) |
|
492 apply(clarify) |
|
493 apply(drule_tac x="Suc a # lista" in bspec) |
|
494 apply(simp) |
|
495 apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
|
496 apply(case_tac q) |
|
497 apply(simp add: PosOrd_def pflat_len_simps) |
|
498 apply(clarify) |
|
499 apply(drule_tac x="Suc a # lista" in bspec) |
|
500 apply(simp) |
|
501 apply(auto simp add: PosOrd_def pflat_len_simps)[1] |
|
502 done |
|
503 |
|
504 lemma PosOrd_Stars_appendE: |
|
505 assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
506 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
507 using assms |
|
508 apply(induct vs) |
|
509 apply(simp) |
|
510 apply(simp add: PosOrd_StarsE2) |
|
511 done |
|
512 |
|
513 lemma PosOrd_Stars_append_eq: |
|
514 assumes "flats vs1 = flats vs2" |
|
515 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
|
516 using assms |
|
517 apply(rule_tac iffI) |
|
518 apply(erule PosOrd_Stars_appendE) |
|
519 apply(rule PosOrd_Stars_appendI) |
|
520 apply(auto) |
|
521 done |
|
522 |
|
523 lemma PosOrd_almost_trichotomous: |
|
524 shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (length (flat v1) = length (flat v2))" |
|
525 apply(auto simp add: PosOrd_ex_def) |
|
526 apply(auto simp add: PosOrd_def) |
|
527 apply(rule_tac x="[]" in exI) |
|
528 apply(auto simp add: Pos_empty pflat_len_simps) |
|
529 apply(drule_tac x="[]" in spec) |
|
530 apply(auto simp add: Pos_empty pflat_len_simps) |
|
531 done |
|
532 |
|
533 |
|
534 |
|
535 section {* The Posix Value is smaller than any other Value *} |
|
536 |
|
537 |
|
538 lemma Posix_PosOrd: |
|
539 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> LV r s" |
|
540 shows "v1 :\<sqsubseteq>val v2" |
|
541 using assms |
|
542 proof (induct arbitrary: v2 rule: Posix.induct) |
|
543 case (Posix_ONE v) |
|
544 have "v \<in> LV ONE []" by fact |
|
545 then have "v = Void" |
|
546 by (simp add: LV_simps) |
|
547 then show "Void :\<sqsubseteq>val v" |
|
548 by (simp add: PosOrd_ex_eq_def) |
|
549 next |
|
550 case (Posix_CHAR c v) |
|
551 have "v \<in> LV (CHAR c) [c]" by fact |
|
552 then have "v = Char c" |
|
553 by (simp add: LV_simps) |
|
554 then show "Char c :\<sqsubseteq>val v" |
|
555 by (simp add: PosOrd_ex_eq_def) |
|
556 next |
|
557 case (Posix_ALT1 s r1 v r2 v2) |
|
558 have as1: "s \<in> r1 \<rightarrow> v" by fact |
|
559 have IH: "\<And>v2. v2 \<in> LV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
|
560 have "v2 \<in> LV (ALT r1 r2) s" by fact |
|
561 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
|
562 by(auto simp add: LV_def prefix_list_def) |
|
563 then consider |
|
564 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
|
565 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
|
566 by (auto elim: Prf.cases) |
|
567 then show "Left v :\<sqsubseteq>val v2" |
|
568 proof(cases) |
|
569 case (Left v3) |
|
570 have "v3 \<in> LV r1 s" using Left(2,3) |
|
571 by (auto simp add: LV_def prefix_list_def) |
|
572 with IH have "v :\<sqsubseteq>val v3" by simp |
|
573 moreover |
|
574 have "flat v3 = flat v" using as1 Left(3) |
|
575 by (simp add: Posix1(2)) |
|
576 ultimately have "Left v :\<sqsubseteq>val Left v3" |
|
577 by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq) |
|
578 then show "Left v :\<sqsubseteq>val v2" unfolding Left . |
|
579 next |
|
580 case (Right v3) |
|
581 have "flat v3 = flat v" using as1 Right(3) |
|
582 by (simp add: Posix1(2)) |
|
583 then have "Left v :\<sqsubseteq>val Right v3" |
|
584 unfolding PosOrd_ex_eq_def |
|
585 by (simp add: PosOrd_Left_Right) |
|
586 then show "Left v :\<sqsubseteq>val v2" unfolding Right . |
|
587 qed |
|
588 next |
|
589 case (Posix_ALT2 s r2 v r1 v2) |
|
590 have as1: "s \<in> r2 \<rightarrow> v" by fact |
|
591 have as2: "s \<notin> L r1" by fact |
|
592 have IH: "\<And>v2. v2 \<in> LV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact |
|
593 have "v2 \<in> LV (ALT r1 r2) s" by fact |
|
594 then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s" |
|
595 by(auto simp add: LV_def prefix_list_def) |
|
596 then consider |
|
597 (Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s" |
|
598 | (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s" |
|
599 by (auto elim: Prf.cases) |
|
600 then show "Right v :\<sqsubseteq>val v2" |
|
601 proof (cases) |
|
602 case (Right v3) |
|
603 have "v3 \<in> LV r2 s" using Right(2,3) |
|
604 by (auto simp add: LV_def prefix_list_def) |
|
605 with IH have "v :\<sqsubseteq>val v3" by simp |
|
606 moreover |
|
607 have "flat v3 = flat v" using as1 Right(3) |
|
608 by (simp add: Posix1(2)) |
|
609 ultimately have "Right v :\<sqsubseteq>val Right v3" |
|
610 by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI) |
|
611 then show "Right v :\<sqsubseteq>val v2" unfolding Right . |
|
612 next |
|
613 case (Left v3) |
|
614 have "v3 \<in> LV r1 s" using Left(2,3) as2 |
|
615 by (auto simp add: LV_def prefix_list_def) |
|
616 then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3) |
|
617 by (simp add: Posix1(2) LV_def) |
|
618 then have "False" using as1 as2 Left |
|
619 by (auto simp add: Posix1(2) L_flat_Prf1) |
|
620 then show "Right v :\<sqsubseteq>val v2" by simp |
|
621 qed |
|
622 next |
|
623 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3) |
|
624 have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+ |
|
625 then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2)) |
|
626 have IH1: "\<And>v3. v3 \<in> LV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact |
|
627 have IH2: "\<And>v3. v3 \<in> LV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact |
|
628 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact |
|
629 have "v3 \<in> LV (SEQ r1 r2) (s1 @ s2)" by fact |
|
630 then obtain v3a v3b where eqs: |
|
631 "v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2" |
|
632 "flat v3a @ flat v3b = s1 @ s2" |
|
633 by (force simp add: prefix_list_def LV_def elim: Prf.cases) |
|
634 with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def |
|
635 by (smt L_flat_Prf1 append_eq_append_conv2 append_self_conv) |
|
636 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs |
|
637 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
638 then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)" |
|
639 using PosOrd_spreI as1(1) eqs by blast |
|
640 then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> LV r1 s1 \<and> v3b \<in> LV r2 s2)" using eqs(2,3) |
|
641 by (auto simp add: LV_def) |
|
642 then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast |
|
643 then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1 |
|
644 unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_Seq_eq) |
|
645 then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast |
|
646 next |
|
647 case (Posix_STAR1 s1 r v s2 vs v3) |
|
648 have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+ |
|
649 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
|
650 have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
|
651 have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
|
652 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact |
|
653 have cond2: "flat v \<noteq> []" by fact |
|
654 have "v3 \<in> LV (STAR r) (s1 @ s2)" by fact |
|
655 then consider |
|
656 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
|
657 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r" |
|
658 "flat (Stars (v3a # vs3)) = s1 @ s2" |
|
659 | (Empty) "v3 = Stars []" |
|
660 unfolding LV_def |
|
661 apply(auto) |
|
662 apply(erule Prf.cases) |
|
663 apply(auto) |
|
664 apply(case_tac vs) |
|
665 apply(auto intro: Prf.intros) |
|
666 done |
|
667 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
668 proof (cases) |
|
669 case (NonEmpty v3a vs3) |
|
670 have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . |
|
671 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
|
672 unfolding prefix_list_def |
|
673 by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) |
|
674 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
|
675 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
676 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
|
677 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
|
678 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" |
|
679 using NonEmpty(2,3) by (auto simp add: LV_def) |
|
680 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
681 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
682 unfolding PosOrd_ex_eq_def by auto |
|
683 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
|
684 unfolding PosOrd_ex_eq_def |
|
685 using PosOrd_StarsI PosOrd_StarsI2 by auto |
|
686 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
|
687 next |
|
688 case Empty |
|
689 have "v3 = Stars []" by fact |
|
690 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
691 unfolding PosOrd_ex_eq_def using cond2 |
|
692 by (simp add: PosOrd_shorterI) |
|
693 qed |
|
694 next |
|
695 case (Posix_STAR2 r v2) |
|
696 have "v2 \<in> LV (STAR r) []" by fact |
|
697 then have "v2 = Stars []" |
|
698 unfolding LV_def by (auto elim: Prf.cases) |
|
699 then show "Stars [] :\<sqsubseteq>val v2" |
|
700 by (simp add: PosOrd_ex_eq_def) |
|
701 next |
|
702 case (Posix_NTIMES1 s1 r v s2 n vs v3) |
|
703 have "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" by fact+ |
|
704 then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2)) |
|
705 have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
|
706 have IH2: "\<And>v3. v3 \<in> LV (NTIMES r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
|
707 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" by fact |
|
708 have cond2: "flat v \<noteq> []" by fact |
|
709 have "v3 \<in> LV (NTIMES r n) (s1 @ s2)" by fact |
|
710 then consider |
|
711 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
|
712 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : NTIMES r (n - 1)" |
|
713 "flats (v3a # vs3) = s1 @ s2" |
|
714 | (Empty) "v3 = Stars []" |
|
715 unfolding LV_def |
|
716 apply(auto) |
|
717 apply(erule Prf.cases) |
|
718 apply(auto) |
|
719 apply(case_tac vs1) |
|
720 apply(auto intro: Prf.intros) |
|
721 apply(case_tac vs2) |
|
722 apply(auto intro: Prf.intros) |
|
723 apply (simp add: as1(1) cond2 flats_empty) |
|
724 by (simp add: Prf.intros(8)) |
|
725 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
726 proof (cases) |
|
727 case (NonEmpty v3a vs3) |
|
728 have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . |
|
729 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
|
730 unfolding prefix_list_def |
|
731 by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars) |
|
732 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
|
733 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
734 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
|
735 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
|
736 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (NTIMES r (n - 1)) s2)" |
|
737 using NonEmpty(2,3) by (auto simp add: LV_def) |
|
738 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
739 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
740 unfolding PosOrd_ex_eq_def by auto |
|
741 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
|
742 unfolding PosOrd_ex_eq_def |
|
743 using PosOrd_StarsI PosOrd_StarsI2 by auto |
|
744 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
|
745 next |
|
746 case Empty |
|
747 have "v3 = Stars []" by fact |
|
748 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
749 unfolding PosOrd_ex_eq_def using cond2 |
|
750 by (simp add: PosOrd_shorterI) |
|
751 qed |
|
752 next |
|
753 case (Posix_NTIMES2 vs r n v2) |
|
754 then show "Stars vs :\<sqsubseteq>val v2" |
|
755 apply(simp add: LV_def) |
|
756 apply(auto) |
|
757 apply(erule Prf_elims) |
|
758 apply(auto) |
|
759 apply(rule PosOrd_eq_Stars_zipI) |
|
760 prefer 2 |
|
761 apply(simp) |
|
762 prefer 2 |
|
763 apply (metis Posix1(2) flats_empty) |
|
764 apply(auto) |
|
765 by (meson in_set_zipE) |
|
766 next |
|
767 case (Posix_UPNTIMES2 r n v2) |
|
768 then show "Stars [] :\<sqsubseteq>val v2" |
|
769 apply(simp add: LV_def) |
|
770 apply(auto) |
|
771 apply(erule Prf_elims) |
|
772 apply(auto) |
|
773 unfolding PosOrd_ex_eq_def by simp |
|
774 next |
|
775 case (Posix_UPNTIMES1 s1 r v s2 n vs v3) |
|
776 have "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (n - 1) \<rightarrow> Stars vs" by fact+ |
|
777 then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2)) |
|
778 have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
|
779 have IH2: "\<And>v3. v3 \<in> LV (UPNTIMES r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
|
780 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (n - 1)))" by fact |
|
781 have cond2: "flat v \<noteq> []" by fact |
|
782 have "v3 \<in> LV (UPNTIMES r n) (s1 @ s2)" by fact |
|
783 then consider |
|
784 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
|
785 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : UPNTIMES r (n - 1)" |
|
786 "flats (v3a # vs3) = s1 @ s2" |
|
787 | (Empty) "v3 = Stars []" |
|
788 unfolding LV_def |
|
789 apply(auto) |
|
790 apply(erule Prf.cases) |
|
791 apply(auto) |
|
792 apply(case_tac vs) |
|
793 apply(auto intro: Prf.intros) |
|
794 by (simp add: Prf.intros(7) as1(1) cond2) |
|
795 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
796 proof (cases) |
|
797 case (NonEmpty v3a vs3) |
|
798 have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . |
|
799 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
|
800 unfolding prefix_list_def |
|
801 apply(simp) |
|
802 apply(simp add: append_eq_append_conv2) |
|
803 apply(auto) |
|
804 by (metis L_flat_Prf1 One_nat_def cond flat_Stars) |
|
805 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
|
806 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
807 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
|
808 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
|
809 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (UPNTIMES r (n - 1)) s2)" |
|
810 using NonEmpty(2,3) by (auto simp add: LV_def) |
|
811 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
812 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
813 unfolding PosOrd_ex_eq_def by auto |
|
814 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
|
815 unfolding PosOrd_ex_eq_def |
|
816 using PosOrd_StarsI PosOrd_StarsI2 by auto |
|
817 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
|
818 next |
|
819 case Empty |
|
820 have "v3 = Stars []" by fact |
|
821 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
822 unfolding PosOrd_ex_eq_def using cond2 |
|
823 by (simp add: PosOrd_shorterI) |
|
824 qed |
|
825 next |
|
826 case (Posix_FROMNTIMES2 vs r n v2) |
|
827 then show "Stars vs :\<sqsubseteq>val v2" |
|
828 apply(simp add: LV_def) |
|
829 apply(auto) |
|
830 apply(erule Prf_elims) |
|
831 apply(auto) |
|
832 apply(rule PosOrd_eq_Stars_zipI) |
|
833 prefer 2 |
|
834 apply(simp) |
|
835 prefer 2 |
|
836 apply (metis Posix1(2) flats_empty) |
|
837 apply(auto) |
|
838 by (meson in_set_zipE) |
|
839 next |
|
840 case (Posix_FROMNTIMES1 s1 r v s2 n vs v3) |
|
841 have "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" by fact+ |
|
842 then have as1: "s1 = flat v" "s2 = flats vs" by (auto dest: Posix1(2)) |
|
843 have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact |
|
844 have IH2: "\<And>v3. v3 \<in> LV (FROMNTIMES r (n - 1)) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact |
|
845 have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))" by fact |
|
846 have cond2: "flat v \<noteq> []" by fact |
|
847 have "v3 \<in> LV (FROMNTIMES r n) (s1 @ s2)" by fact |
|
848 then consider |
|
849 (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" |
|
850 "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : FROMNTIMES r (n - 1)" |
|
851 "flats (v3a # vs3) = s1 @ s2" |
|
852 | (Empty) "v3 = Stars []" |
|
853 unfolding LV_def |
|
854 apply(auto) |
|
855 apply(erule Prf.cases) |
|
856 apply(auto) |
|
857 apply(case_tac vs1) |
|
858 apply(auto intro: Prf.intros) |
|
859 apply(case_tac vs2) |
|
860 apply(auto intro: Prf.intros) |
|
861 apply (simp add: as1(1) cond2 flats_empty) |
|
862 apply (simp add: Prf.intros) |
|
863 apply(case_tac vs) |
|
864 apply(auto) |
|
865 using Posix_FROMNTIMES1.hyps(6) Prf.intros(10) by auto |
|
866 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
867 proof (cases) |
|
868 case (NonEmpty v3a vs3) |
|
869 have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . |
|
870 with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3) |
|
871 unfolding prefix_list_def |
|
872 by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7) flat_Stars) |
|
873 then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4) |
|
874 by (simp add: sprefix_list_def append_eq_conv_conj) |
|
875 then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" |
|
876 using PosOrd_spreI as1(1) NonEmpty(4) by blast |
|
877 then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (FROMNTIMES r (n - 1)) s2)" |
|
878 using NonEmpty(2,3) by (auto simp add: LV_def) |
|
879 then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast |
|
880 then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" |
|
881 unfolding PosOrd_ex_eq_def by auto |
|
882 then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1 |
|
883 unfolding PosOrd_ex_eq_def |
|
884 using PosOrd_StarsI PosOrd_StarsI2 by auto |
|
885 then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast |
|
886 next |
|
887 case Empty |
|
888 have "v3 = Stars []" by fact |
|
889 then show "Stars (v # vs) :\<sqsubseteq>val v3" |
|
890 unfolding PosOrd_ex_eq_def using cond2 |
|
891 by (simp add: PosOrd_shorterI) |
|
892 qed |
|
893 next |
|
894 case (Posix_NMTIMES2 vs r n m v2) |
|
895 then show "Stars vs :\<sqsubseteq>val v2" sorry |
|
896 next |
|
897 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
|
898 then show "Stars (v # vs) :\<sqsubseteq>val v2" sorry |
|
899 qed |
|
900 |
|
901 |
|
902 lemma Posix_PosOrd_reverse: |
|
903 assumes "s \<in> r \<rightarrow> v1" |
|
904 shows "\<not>(\<exists>v2 \<in> LV r s. v2 :\<sqsubset>val v1)" |
|
905 using assms |
|
906 by (metis Posix_PosOrd less_irrefl PosOrd_def |
|
907 PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) |
|
908 |
|
909 lemma PosOrd_Posix: |
|
910 assumes "v1 \<in> LV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1" |
|
911 shows "s \<in> r \<rightarrow> v1" |
|
912 proof - |
|
913 have "s \<in> L r" using assms(1) unfolding LV_def |
|
914 using L_flat_Prf1 by blast |
|
915 then obtain vposix where vp: "s \<in> r \<rightarrow> vposix" |
|
916 using lexer_correct_Some by blast |
|
917 with assms(1) have "vposix :\<sqsubseteq>val v1" by (simp add: Posix_PosOrd) |
|
918 then have "vposix = v1 \<or> vposix :\<sqsubset>val v1" unfolding PosOrd_ex_eq2 by auto |
|
919 moreover |
|
920 { assume "vposix :\<sqsubset>val v1" |
|
921 moreover |
|
922 have "vposix \<in> LV r s" using vp |
|
923 using Posix_LV by blast |
|
924 ultimately have "False" using assms(2) by blast |
|
925 } |
|
926 ultimately show "s \<in> r \<rightarrow> v1" using vp by blast |
|
927 qed |
|
928 |
|
929 lemma Least_existence: |
|
930 assumes "LV r s \<noteq> {}" |
|
931 shows " \<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
932 proof - |
|
933 from assms |
|
934 obtain vposix where "s \<in> r \<rightarrow> vposix" |
|
935 unfolding LV_def |
|
936 using L_flat_Prf1 lexer_correct_Some by blast |
|
937 then have "\<forall>v \<in> LV r s. vposix :\<sqsubseteq>val v" |
|
938 by (simp add: Posix_PosOrd) |
|
939 then show "\<exists>vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
940 using Posix_LV \<open>s \<in> r \<rightarrow> vposix\<close> by blast |
|
941 qed |
|
942 |
|
943 lemma Least_existence1: |
|
944 assumes "LV r s \<noteq> {}" |
|
945 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> LV r s. vmin :\<sqsubseteq>val v" |
|
946 using Least_existence[OF assms] assms |
|
947 using PosOrdeq_antisym by blast |
|
948 |
|
949 |
|
950 |
|
951 |
|
952 |
|
953 lemma Least_existence1_pre: |
|
954 assumes "LV r s \<noteq> {}" |
|
955 shows " \<exists>!vmin \<in> LV r s. \<forall>v \<in> (LV r s \<union> {v'. flat v' \<sqsubset>spre s}). vmin :\<sqsubseteq>val v" |
|
956 using Least_existence[OF assms] assms |
|
957 apply - |
|
958 apply(erule bexE) |
|
959 apply(rule_tac a="vmin" in ex1I) |
|
960 apply(auto)[1] |
|
961 apply (metis PosOrd_Posix PosOrd_ex_eq2 PosOrd_spreI PosOrdeq_antisym Posix1(2)) |
|
962 apply(auto)[1] |
|
963 apply(simp add: PosOrdeq_antisym) |
|
964 done |
|
965 |
|
966 lemma |
|
967 shows "partial_order_on UNIV {(v1, v2). v1 :\<sqsubseteq>val v2}" |
|
968 apply(simp add: partial_order_on_def) |
|
969 apply(simp add: preorder_on_def refl_on_def) |
|
970 apply(simp add: PosOrdeq_refl) |
|
971 apply(auto) |
|
972 apply(rule transI) |
|
973 apply(auto intro: PosOrdeq_trans)[1] |
|
974 apply(rule antisymI) |
|
975 apply(simp add: PosOrdeq_antisym) |
|
976 done |
|
977 |
|
978 lemma |
|
979 "wf {(v1, v2). v1 :\<sqsubset>val v2 \<and> v1 \<in> LV r s \<and> v2 \<in> LV r s}" |
|
980 apply(rule finite_acyclic_wf) |
|
981 prefer 2 |
|
982 apply(simp add: acyclic_def) |
|
983 apply(induct_tac rule: trancl.induct) |
|
984 apply(auto)[1] |
|
985 oops |
|
986 |
|
987 |
|
988 unused_thms |
|
989 |
|
990 end |