1 |
1 |
2 theory Sulzmann |
2 theory Sulzmann |
3 imports "Lexer" "~~/src/HOL/Library/Multiset" |
3 imports "Positions" |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Sulzmann's "Ordering" of Values *} |
7 section {* Sulzmann's "Ordering" of Values *} |
8 |
|
9 fun |
|
10 size :: "val \<Rightarrow> nat" |
|
11 where |
|
12 "size (Void) = 0" |
|
13 | "size (Char c) = 0" |
|
14 | "size (Left v) = 1 + size v" |
|
15 | "size (Right v) = 1 + size v" |
|
16 | "size (Seq v1 v2) = 1 + (size v1) + (size v2)" |
|
17 | "size (Stars []) = 0" |
|
18 | "size (Stars (v#vs)) = 1 + (size v) + (size (Stars vs))" |
|
19 |
|
20 lemma Star_size [simp]: |
|
21 "\<lbrakk>n < length vs; 0 < length vs\<rbrakk> \<Longrightarrow> size (nth vs n) < size (Stars vs)" |
|
22 apply(induct vs arbitrary: n) |
|
23 apply(simp) |
|
24 apply(auto) |
|
25 by (metis One_nat_def Suc_pred less_Suc0 less_Suc_eq list.size(3) not_add_less1 not_less_eq nth_Cons' trans_less_add2) |
|
26 |
|
27 lemma Star_size0 [simp]: |
|
28 "0 < length vs \<Longrightarrow> 0 < size (Stars vs)" |
|
29 apply(induct vs) |
|
30 apply(auto) |
|
31 done |
|
32 |
|
33 |
|
34 fun |
|
35 at :: "val \<Rightarrow> nat list \<Rightarrow> val" |
|
36 where |
|
37 "at v [] = v" |
|
38 | "at (Left v) (0#ps)= at v ps" |
|
39 | "at (Right v) (Suc 0#ps)= at v ps" |
|
40 | "at (Seq v1 v2) (0#ps)= at v1 ps" |
|
41 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps" |
|
42 | "at (Stars vs) (n#ps)= at (nth vs n) ps" |
|
43 |
|
44 fun |
|
45 ato :: "val \<Rightarrow> nat list \<Rightarrow> val option" |
|
46 where |
|
47 "ato v [] = Some v" |
|
48 | "ato (Left v) (0#ps)= ato v ps" |
|
49 | "ato (Right v) (Suc 0#ps)= ato v ps" |
|
50 | "ato (Seq v1 v2) (0#ps)= ato v1 ps" |
|
51 | "ato (Seq v1 v2) (Suc 0#ps)= ato v2 ps" |
|
52 | "ato (Stars vs) (n#ps)= (if (n < length vs) then ato (nth vs n) ps else None)" |
|
53 | "ato v p = None" |
|
54 |
|
55 fun Pos :: "val \<Rightarrow> (nat list) set" |
|
56 where |
|
57 "Pos (Void) = {[]}" |
|
58 | "Pos (Char c) = {[]}" |
|
59 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}" |
|
60 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}" |
|
61 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" |
|
62 | "Pos (Stars []) = {[]}" |
|
63 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {(Suc n)#ps | n ps. n#ps \<in> Pos (Stars vs)}" |
|
64 |
|
65 lemma Pos_empty: |
|
66 shows "[] \<in> Pos v" |
|
67 apply(induct v rule: Pos.induct) |
|
68 apply(auto) |
|
69 done |
|
70 |
|
71 lemma Pos_finite_aux: |
|
72 assumes "\<forall>v \<in> set vs. finite (Pos v)" |
|
73 shows "finite (Pos (Stars vs))" |
|
74 using assms |
|
75 apply(induct vs) |
|
76 apply(simp) |
|
77 apply(simp) |
|
78 apply(subgoal_tac "finite (Pos (Stars vs) - {[]})") |
|
79 apply(rule_tac f="\<lambda>l. Suc (hd l) # tl l" in finite_surj) |
|
80 apply(assumption) |
|
81 back |
|
82 apply(auto simp add: image_def) |
|
83 apply(rule_tac x="n#ps" in bexI) |
|
84 apply(simp) |
|
85 apply(simp) |
|
86 done |
|
87 |
|
88 lemma Pos_finite: |
|
89 shows "finite (Pos v)" |
|
90 apply(induct v rule: val.induct) |
|
91 apply(auto) |
|
92 apply(simp add: Pos_finite_aux) |
|
93 done |
|
94 |
|
95 |
|
96 lemma ato_test: |
|
97 assumes "p \<in> Pos v" |
|
98 shows "\<exists>v'. ato v p = Some v'" |
|
99 using assms |
|
100 apply(induct v arbitrary: p rule: Pos.induct) |
|
101 apply(auto) |
|
102 apply force |
|
103 by (metis ato.simps(6) option.distinct(1)) |
|
104 |
|
105 definition pflat :: "val \<Rightarrow> nat list => string option" |
|
106 where |
|
107 "pflat v p \<equiv> (if p \<in> Pos v then Some (flat (at v p)) else None)" |
|
108 |
|
109 fun intlen :: "'a list \<Rightarrow> int" |
|
110 where |
|
111 "intlen [] = 0" |
|
112 | "intlen (x#xs) = 1 + intlen xs" |
|
113 |
|
114 lemma inlen_bigger: |
|
115 shows "0 \<le> intlen xs" |
|
116 apply(induct xs) |
|
117 apply(auto) |
|
118 done |
|
119 |
|
120 lemma intlen_append: |
|
121 shows "intlen (xs @ ys) = intlen xs + intlen ys" |
|
122 apply(induct xs arbitrary: ys) |
|
123 apply(auto) |
|
124 done |
|
125 |
|
126 lemma intlen_length: |
|
127 assumes "length xs < length ys" |
|
128 shows "intlen xs < intlen ys" |
|
129 using assms |
|
130 apply(induct xs arbitrary: ys) |
|
131 apply(auto) |
|
132 apply(case_tac ys) |
|
133 apply(simp_all) |
|
134 apply (smt inlen_bigger) |
|
135 by (smt Suc_lessE intlen.simps(2) length_Suc_conv) |
|
136 |
|
137 |
|
138 definition pflat_len :: "val \<Rightarrow> nat list => int" |
|
139 where |
|
140 "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)" |
|
141 |
|
142 lemma pflat_len_simps: |
|
143 shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p" |
|
144 and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p" |
|
145 and "pflat_len (Left v) (0#p) = pflat_len v p" |
|
146 and "pflat_len (Left v) (Suc 0#p) = -1" |
|
147 and "pflat_len (Right v) (Suc 0#p) = pflat_len v p" |
|
148 and "pflat_len (Right v) (0#p) = -1" |
|
149 and "pflat_len v [] = intlen (flat v)" |
|
150 apply(auto simp add: pflat_len_def Pos_empty) |
|
151 done |
|
152 |
|
153 lemma pflat_len_Stars_simps: |
|
154 assumes "n < length vs" |
|
155 shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p" |
|
156 using assms |
|
157 apply(induct vs arbitrary: n p) |
|
158 apply(simp) |
|
159 apply(simp) |
|
160 apply(simp add: pflat_len_def) |
|
161 apply(auto)[1] |
|
162 apply (metis at.simps(6)) |
|
163 apply (metis Suc_less_eq Suc_pred) |
|
164 by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons') |
|
165 |
|
166 |
|
167 lemma pflat_len_Stars_simps2: |
|
168 shows "pflat_len (Stars (v#vs)) (Suc n # p) = pflat_len (Stars vs) (n#p)" |
|
169 and "pflat_len (Stars (v#vs)) (0 # p) = pflat_len v p" |
|
170 using assms |
|
171 apply(simp_all add: pflat_len_def) |
|
172 done |
|
173 |
|
174 lemma Two_to_Three_aux: |
|
175 assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p" |
|
176 shows "p \<in> Pos v1 \<inter> Pos v2" |
|
177 using assms |
|
178 apply(simp add: pflat_len_def) |
|
179 apply(auto split: if_splits) |
|
180 apply (smt inlen_bigger)+ |
|
181 done |
|
182 |
|
183 lemma Two_to_Three: |
|
184 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat v1 p = pflat v2 p" |
|
185 shows "Pos v1 = Pos v2" |
|
186 using assms |
|
187 by (metis Un_iff option.distinct(1) pflat_def subsetI subset_antisym) |
|
188 |
|
189 lemma Two_to_Three_orig: |
|
190 assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p" |
|
191 shows "Pos v1 = Pos v2" |
|
192 using assms |
|
193 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym) |
|
194 |
|
195 lemma set_eq1: |
|
196 assumes "insert [] A = insert [] B" "[] \<notin> A" "[] \<notin> B" |
|
197 shows "A = B" |
|
198 using assms |
|
199 by (simp add: insert_ident) |
|
200 |
|
201 lemma set_eq2: |
|
202 assumes "A \<union> B = A \<union> C" |
|
203 and "A \<inter> B = {}" "A \<inter> C = {}" |
|
204 shows "B = C" |
|
205 using assms |
|
206 using Un_Int_distrib sup_bot.left_neutral sup_commute by blast |
|
207 |
|
208 |
|
209 |
|
210 lemma Three_to_One: |
|
211 assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" |
|
212 and "Pos v1 = Pos v2" |
|
213 shows "v1 = v2" |
|
214 using assms |
|
215 apply(induct v1 arbitrary: r v2 rule: Pos.induct) |
|
216 apply(erule Prf.cases) |
|
217 apply(simp_all) |
|
218 apply(erule Prf.cases) |
|
219 apply(simp_all) |
|
220 apply(erule Prf.cases) |
|
221 apply(simp_all) |
|
222 apply(erule Prf.cases) |
|
223 apply(simp_all) |
|
224 apply(erule Prf.cases) |
|
225 apply(simp_all) |
|
226 apply(erule Prf.cases) |
|
227 apply(simp_all) |
|
228 apply(clarify) |
|
229 apply(simp add: insert_ident) |
|
230 apply(drule_tac x="r1a" in meta_spec) |
|
231 apply(drule_tac x="v1a" in meta_spec) |
|
232 apply(simp) |
|
233 apply(drule_tac meta_mp) |
|
234 thm subset_antisym |
|
235 apply(rule subset_antisym) |
|
236 apply(auto)[3] |
|
237 apply(clarify) |
|
238 apply(simp add: insert_ident) |
|
239 using Pos_empty apply blast |
|
240 apply(erule Prf.cases) |
|
241 apply(simp_all) |
|
242 apply(erule Prf.cases) |
|
243 apply(simp_all) |
|
244 apply(clarify) |
|
245 apply(simp add: insert_ident) |
|
246 using Pos_empty apply blast |
|
247 apply(simp add: insert_ident) |
|
248 apply(drule_tac x="r2a" in meta_spec) |
|
249 apply(drule_tac x="v2b" in meta_spec) |
|
250 apply(simp) |
|
251 apply(drule_tac meta_mp) |
|
252 apply(rule subset_antisym) |
|
253 apply(auto)[3] |
|
254 apply(erule Prf.cases) |
|
255 apply(simp_all) |
|
256 apply(erule Prf.cases) |
|
257 apply(simp_all) |
|
258 apply(simp add: insert_ident) |
|
259 apply(clarify) |
|
260 apply(drule_tac x="r1a" in meta_spec) |
|
261 apply(drule_tac x="r2a" in meta_spec) |
|
262 apply(drule_tac x="v1b" in meta_spec) |
|
263 apply(drule_tac x="v2c" in meta_spec) |
|
264 apply(simp) |
|
265 apply(drule_tac meta_mp) |
|
266 apply(rule subset_antisym) |
|
267 apply(rule subsetI) |
|
268 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}") |
|
269 prefer 2 |
|
270 apply(auto)[1] |
|
271 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}") |
|
272 prefer 2 |
|
273 apply (metis (no_types, lifting) Un_iff) |
|
274 apply(simp) |
|
275 apply(rule subsetI) |
|
276 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}") |
|
277 prefer 2 |
|
278 apply(auto)[1] |
|
279 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}") |
|
280 prefer 2 |
|
281 apply (metis (no_types, lifting) Un_iff) |
|
282 apply(simp (no_asm_use)) |
|
283 apply(simp) |
|
284 apply(drule_tac meta_mp) |
|
285 apply(rule subset_antisym) |
|
286 apply(rule subsetI) |
|
287 apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2b}") |
|
288 prefer 2 |
|
289 apply(auto)[1] |
|
290 apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}") |
|
291 prefer 2 |
|
292 apply (metis (no_types, lifting) Un_iff) |
|
293 apply(simp) |
|
294 apply(rule subsetI) |
|
295 apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2c}") |
|
296 prefer 2 |
|
297 apply(auto)[1] |
|
298 apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}") |
|
299 prefer 2 |
|
300 apply (metis (no_types, lifting) Un_iff) |
|
301 apply(simp (no_asm_use)) |
|
302 apply(simp) |
|
303 apply(erule Prf.cases) |
|
304 apply(simp_all) |
|
305 apply(erule Prf.cases) |
|
306 apply(simp_all) |
|
307 apply(auto)[1] |
|
308 using Pos_empty apply fastforce |
|
309 apply(erule Prf.cases) |
|
310 apply(simp_all) |
|
311 apply(erule Prf.cases) |
|
312 apply(simp_all) |
|
313 apply(auto)[1] |
|
314 using Pos_empty apply fastforce |
|
315 apply(clarify) |
|
316 apply(simp add: insert_ident) |
|
317 apply(drule_tac x="rb" in meta_spec) |
|
318 apply(drule_tac x="STAR rb" in meta_spec) |
|
319 apply(drule_tac x="vb" in meta_spec) |
|
320 apply(drule_tac x="Stars vsb" in meta_spec) |
|
321 apply(simp) |
|
322 apply(drule_tac meta_mp) |
|
323 apply(rule subset_antisym) |
|
324 apply(rule subsetI) |
|
325 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va}") |
|
326 prefer 2 |
|
327 apply(auto)[1] |
|
328 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}") |
|
329 prefer 2 |
|
330 apply (metis (no_types, lifting) Un_iff) |
|
331 apply(simp) |
|
332 apply(rule subsetI) |
|
333 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb}") |
|
334 prefer 2 |
|
335 apply(auto)[1] |
|
336 apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}") |
|
337 prefer 2 |
|
338 apply (metis (no_types, lifting) Un_iff) |
|
339 apply(simp (no_asm_use)) |
|
340 apply(simp) |
|
341 apply(drule_tac meta_mp) |
|
342 apply(rule subset_antisym) |
|
343 apply(rule subsetI) |
|
344 apply(case_tac vsa) |
|
345 apply(simp) |
|
346 apply (simp add: Pos_empty) |
|
347 apply(simp) |
|
348 apply(clarify) |
|
349 apply(erule disjE) |
|
350 apply (simp add: Pos_empty) |
|
351 apply(erule disjE) |
|
352 apply(clarify) |
|
353 apply(subgoal_tac |
|
354 "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
355 prefer 2 |
|
356 apply blast |
|
357 apply(subgoal_tac "Suc 0 # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}") |
|
358 prefer 2 |
|
359 apply (metis (no_types, lifting) Un_iff) |
|
360 apply(simp) |
|
361 apply(clarify) |
|
362 apply(subgoal_tac |
|
363 "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
364 prefer 2 |
|
365 apply blast |
|
366 apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}") |
|
367 prefer 2 |
|
368 apply (metis (no_types, lifting) Un_iff) |
|
369 apply(simp) |
|
370 apply(rule subsetI) |
|
371 apply(case_tac vsb) |
|
372 apply(simp) |
|
373 apply (simp add: Pos_empty) |
|
374 apply(simp) |
|
375 apply(clarify) |
|
376 apply(erule disjE) |
|
377 apply (simp add: Pos_empty) |
|
378 apply(erule disjE) |
|
379 apply(clarify) |
|
380 apply(subgoal_tac |
|
381 "Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
382 prefer 2 |
|
383 apply(simp) |
|
384 apply(subgoal_tac "Suc 0 # ps \<in> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}") |
|
385 apply blast |
|
386 using list.inject apply blast |
|
387 apply(clarify) |
|
388 apply(subgoal_tac |
|
389 "Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}") |
|
390 prefer 2 |
|
391 apply(simp) |
|
392 apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}") |
|
393 prefer 2 |
|
394 apply (metis (no_types, lifting) Un_iff) |
|
395 apply(simp (no_asm_use)) |
|
396 apply(simp) |
|
397 done |
|
398 |
|
399 definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _") |
|
400 where |
|
401 "ps1 \<sqsubseteq>pre ps2 \<equiv> (\<exists>ps'. ps1 @ps' = ps2)" |
|
402 |
|
403 definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _") |
|
404 where |
|
405 "ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)" |
|
406 |
|
407 inductive lex_lists :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _") |
|
408 where |
|
409 "[] \<sqsubset>lex p#ps" |
|
410 | "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)" |
|
411 | "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)" |
|
412 |
|
413 lemma lex_irrfl: |
|
414 fixes ps1 ps2 :: "nat list" |
|
415 assumes "ps1 \<sqsubset>lex ps2" |
|
416 shows "ps1 \<noteq> ps2" |
|
417 using assms |
|
418 apply(induct rule: lex_lists.induct) |
|
419 apply(auto) |
|
420 done |
|
421 |
|
422 lemma lex_append: |
|
423 assumes "ps2 \<noteq> []" |
|
424 shows "ps \<sqsubset>lex ps @ ps2" |
|
425 using assms |
|
426 apply(induct ps) |
|
427 apply(auto intro: lex_lists.intros) |
|
428 apply(case_tac ps2) |
|
429 apply(simp) |
|
430 apply(simp) |
|
431 apply(auto intro: lex_lists.intros) |
|
432 done |
|
433 |
|
434 lemma lexordp_simps [simp]: |
|
435 fixes xs ys :: "nat list" |
|
436 shows "[] \<sqsubset>lex ys = (ys \<noteq> [])" |
|
437 and "xs \<sqsubset>lex [] = False" |
|
438 and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))" |
|
439 apply - |
|
440 apply (metis lex_append lex_lists.simps list.simps(3)) |
|
441 using lex_lists.cases apply blast |
|
442 using lex_lists.cases lex_lists.intros(2) lex_lists.intros(3) not_less_iff_gr_or_eq by fastforce |
|
443 |
|
444 lemma lex_append_cancel [simp]: |
|
445 fixes ps ps1 ps2 :: "nat list" |
|
446 shows "ps @ ps1 \<sqsubset>lex ps @ ps2 \<longleftrightarrow> ps1 \<sqsubset>lex ps2" |
|
447 apply(induct ps) |
|
448 apply(auto) |
|
449 done |
|
450 |
|
451 lemma lex_trans: |
|
452 fixes ps1 ps2 ps3 :: "nat list" |
|
453 assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3" |
|
454 shows "ps1 \<sqsubset>lex ps3" |
|
455 using assms |
|
456 apply(induct arbitrary: ps3 rule: lex_lists.induct) |
|
457 apply(erule lex_lists.cases) |
|
458 apply(simp_all) |
|
459 apply(rotate_tac 2) |
|
460 apply(erule lex_lists.cases) |
|
461 apply(simp_all) |
|
462 apply(erule lex_lists.cases) |
|
463 apply(simp_all) |
|
464 done |
|
465 |
|
466 lemma trichotomous_aux: |
|
467 fixes p q :: "nat list" |
|
468 assumes "p \<sqsubset>lex q" "p \<noteq> q" |
|
469 shows "\<not>(q \<sqsubset>lex p)" |
|
470 using assms |
|
471 apply(induct rule: lex_lists.induct) |
|
472 apply(auto) |
|
473 done |
|
474 |
|
475 lemma trichotomous_aux2: |
|
476 fixes p q :: "nat list" |
|
477 assumes "p \<sqsubset>lex q" "q \<sqsubset>lex p" |
|
478 shows "False" |
|
479 using assms |
|
480 apply(induct rule: lex_lists.induct) |
|
481 apply(auto) |
|
482 done |
|
483 |
|
484 lemma trichotomous: |
|
485 fixes p q :: "nat list" |
|
486 shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p" |
|
487 apply(induct p arbitrary: q) |
|
488 apply(auto) |
|
489 apply(case_tac q) |
|
490 apply(auto) |
|
491 done |
|
492 |
|
493 definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" |
|
494 where |
|
495 "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)" |
|
496 |
|
497 definition |
|
498 "DPos v1 v2 \<equiv> {p. dpos v1 v2 p}" |
|
499 |
|
500 lemma outside_lemma: |
|
501 assumes "p \<notin> Pos v1 \<union> Pos v2" |
|
502 shows "pflat_len v1 p = pflat_len v2 p" |
|
503 using assms |
|
504 apply(auto simp add: pflat_len_def) |
|
505 done |
|
506 |
|
507 lemma dpos_lemma_aux: |
|
508 assumes "p \<in> Pos v1 \<union> Pos v2" |
|
509 and "pflat_len v1 p = pflat_len v2 p" |
|
510 shows "p \<in> Pos v1 \<inter> Pos v2" |
|
511 using assms |
|
512 apply(auto simp add: pflat_len_def) |
|
513 apply (smt inlen_bigger) |
|
514 apply (smt inlen_bigger) |
|
515 done |
|
516 |
|
517 lemma dpos_lemma: |
|
518 assumes "p \<in> Pos v1 \<union> Pos v2" |
|
519 and "pflat_len v1 p = pflat_len v2 p" |
|
520 shows "\<not>dpos v1 v2 p" |
|
521 using assms |
|
522 apply(auto simp add: dpos_def dpos_lemma_aux) |
|
523 using dpos_lemma_aux apply auto[1] |
|
524 using dpos_lemma_aux apply auto[1] |
|
525 done |
|
526 |
|
527 lemma dpos_lemma2: |
|
528 assumes "p \<in> Pos v1 \<union> Pos v2" |
|
529 and "dpos v1 v2 p" |
|
530 shows "pflat_len v1 p \<noteq> pflat_len v2 p" |
|
531 using assms |
|
532 using dpos_lemma by blast |
|
533 |
|
534 lemma DPos_lemma: |
|
535 assumes "p \<in> DPos v1 v2" |
|
536 shows "pflat_len v1 p \<noteq> pflat_len v2 p" |
|
537 using assms |
|
538 unfolding DPos_def |
|
539 apply(auto simp add: pflat_len_def dpos_def) |
|
540 apply (smt inlen_bigger) |
|
541 by (smt inlen_bigger) |
|
542 |
|
543 |
|
544 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _") |
|
545 where |
|
546 "v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and> |
|
547 (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))" |
|
548 |
|
549 |
|
550 definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _") |
|
551 where |
|
552 "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)" |
|
553 |
|
554 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _") |
|
555 where |
|
556 "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2" |
|
557 |
|
558 lemma val_ord_shorterI: |
|
559 assumes "length (flat v') < length (flat v)" |
|
560 shows "v :\<sqsubset>val v'" |
|
561 using assms(1) |
|
562 apply(subst val_ord_ex_def) |
|
563 apply(rule_tac x="[]" in exI) |
|
564 apply(subst val_ord_def) |
|
565 apply(rule conjI) |
|
566 apply (simp add: Pos_empty) |
|
567 apply(rule conjI) |
|
568 apply(simp add: pflat_len_simps) |
|
569 apply (simp add: intlen_length) |
|
570 apply(simp) |
|
571 done |
|
572 |
|
573 lemma val_ord_spre: |
|
574 assumes "(flat v') \<sqsubset>spre (flat v)" |
|
575 shows "v :\<sqsubset>val v'" |
|
576 using assms(1) |
|
577 apply(rule_tac val_ord_shorterI) |
|
578 apply(simp add: sprefix_list_def prefix_list_def) |
|
579 apply(auto) |
|
580 apply(case_tac ps') |
|
581 apply(auto) |
|
582 by (metis append_eq_conv_conj drop_all le_less_linear neq_Nil_conv) |
|
583 |
|
584 |
|
585 lemma val_ord_ALTI: |
|
586 assumes "v \<sqsubset>val p v'" "flat v = flat v'" |
|
587 shows "(Left v) \<sqsubset>val (0#p) (Left v')" |
|
588 using assms(1) |
|
589 apply(subst (asm) val_ord_def) |
|
590 apply(erule conjE) |
|
591 apply(subst val_ord_def) |
|
592 apply(rule conjI) |
|
593 apply(simp) |
|
594 apply(rule conjI) |
|
595 apply(simp add: pflat_len_simps) |
|
596 apply(rule ballI) |
|
597 apply(rule impI) |
|
598 apply(simp only: Pos.simps) |
|
599 apply(auto)[1] |
|
600 using assms(2) |
|
601 apply(simp add: pflat_len_simps) |
|
602 apply(auto simp add: pflat_len_simps)[2] |
|
603 done |
|
604 |
|
605 lemma val_ord_ALTI2: |
|
606 assumes "v \<sqsubset>val p v'" "flat v = flat v'" |
|
607 shows "(Right v) \<sqsubset>val (1#p) (Right v')" |
|
608 using assms(1) |
|
609 apply(subst (asm) val_ord_def) |
|
610 apply(erule conjE) |
|
611 apply(subst val_ord_def) |
|
612 apply(rule conjI) |
|
613 apply(simp) |
|
614 apply(rule conjI) |
|
615 apply(simp add: pflat_len_simps) |
|
616 apply(rule ballI) |
|
617 apply(rule impI) |
|
618 apply(simp only: Pos.simps) |
|
619 apply(auto)[1] |
|
620 using assms(2) |
|
621 apply(simp add: pflat_len_simps) |
|
622 apply(auto simp add: pflat_len_simps)[2] |
|
623 done |
|
624 |
|
625 lemma val_ord_ALTE: |
|
626 assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)" |
|
627 shows "p = 0 \<and> v1 \<sqsubset>val ps v2" |
|
628 using assms(1) |
|
629 apply(simp add: val_ord_def) |
|
630 apply(auto simp add: pflat_len_simps) |
|
631 apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def) |
|
632 by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def) |
|
633 |
|
634 lemma val_ord_ALTE2: |
|
635 assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)" |
|
636 shows "p = 1 \<and> v1 \<sqsubset>val ps v2" |
|
637 using assms(1) |
|
638 apply(simp add: val_ord_def) |
|
639 apply(auto simp add: pflat_len_simps) |
|
640 apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def) |
|
641 by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def) |
|
642 |
|
643 lemma val_ord_STARI: |
|
644 assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))" |
|
645 shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))" |
|
646 using assms(1) |
|
647 apply(subst (asm) val_ord_def) |
|
648 apply(erule conjE) |
|
649 apply(subst val_ord_def) |
|
650 apply(rule conjI) |
|
651 apply(simp) |
|
652 apply(rule conjI) |
|
653 apply(subst pflat_len_Stars_simps) |
|
654 apply(simp) |
|
655 apply(subst pflat_len_Stars_simps) |
|
656 apply(simp) |
|
657 apply(simp) |
|
658 apply(rule ballI) |
|
659 apply(rule impI) |
|
660 apply(simp) |
|
661 apply(auto) |
|
662 using assms(2) |
|
663 apply(simp add: pflat_len_simps) |
|
664 apply(auto simp add: pflat_len_Stars_simps) |
|
665 done |
|
666 |
|
667 lemma val_ord_STARI2: |
|
668 assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)" |
|
669 shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))" |
|
670 using assms(1) |
|
671 apply(subst (asm) val_ord_def) |
|
672 apply(erule conjE)+ |
|
673 apply(subst val_ord_def) |
|
674 apply(rule conjI) |
|
675 apply(simp) |
|
676 apply(rule conjI) |
|
677 apply(case_tac vs1) |
|
678 apply(simp) |
|
679 apply(simp) |
|
680 apply(auto)[1] |
|
681 apply(case_tac vs2) |
|
682 apply(simp) |
|
683 apply (simp add: pflat_len_def) |
|
684 apply(simp) |
|
685 apply(auto)[1] |
|
686 apply (simp add: pflat_len_Stars_simps) |
|
687 using pflat_len_def apply auto[1] |
|
688 apply(rule ballI) |
|
689 apply(rule impI) |
|
690 apply(simp) |
|
691 using assms(2) |
|
692 apply(auto) |
|
693 apply (simp add: pflat_len_simps(7)) |
|
694 apply (simp add: pflat_len_Stars_simps) |
|
695 using assms(2) |
|
696 apply(auto simp add: pflat_len_def)[1] |
|
697 apply force |
|
698 apply force |
|
699 apply(auto simp add: pflat_len_def)[1] |
|
700 apply force |
|
701 apply force |
|
702 apply(auto simp add: pflat_len_def)[1] |
|
703 apply(auto simp add: pflat_len_def)[1] |
|
704 apply force |
|
705 apply force |
|
706 apply(auto simp add: pflat_len_def)[1] |
|
707 apply force |
|
708 apply force |
|
709 done |
|
710 |
|
711 |
|
712 lemma val_ord_SEQI: |
|
713 assumes "v1 \<sqsubset>val p v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
714 shows "(Seq v1 v2) \<sqsubset>val (0#p) (Seq v1' v2')" |
|
715 using assms(1) |
|
716 apply(subst (asm) val_ord_def) |
|
717 apply(erule conjE) |
|
718 apply(subst val_ord_def) |
|
719 apply(rule conjI) |
|
720 apply(simp) |
|
721 apply(rule conjI) |
|
722 apply(simp add: pflat_len_simps) |
|
723 apply(rule ballI) |
|
724 apply(rule impI) |
|
725 apply(simp only: Pos.simps) |
|
726 apply(auto)[1] |
|
727 apply(simp add: pflat_len_simps) |
|
728 using assms(2) |
|
729 apply(simp) |
|
730 apply(auto simp add: pflat_len_simps)[2] |
|
731 done |
|
732 |
|
733 |
|
734 lemma val_ord_SEQI2: |
|
735 assumes "v2 \<sqsubset>val p v2'" "flat v2 = flat v2'" |
|
736 shows "(Seq v v2) \<sqsubset>val (1#p) (Seq v v2')" |
|
737 using assms(1) |
|
738 apply(subst (asm) val_ord_def) |
|
739 apply(erule conjE)+ |
|
740 apply(subst val_ord_def) |
|
741 apply(rule conjI) |
|
742 apply(simp) |
|
743 apply(rule conjI) |
|
744 apply(simp add: pflat_len_simps) |
|
745 apply(rule ballI) |
|
746 apply(rule impI) |
|
747 apply(simp only: Pos.simps) |
|
748 apply(auto) |
|
749 apply(auto simp add: pflat_len_def intlen_append) |
|
750 apply(auto simp add: assms(2)) |
|
751 done |
|
752 |
|
753 lemma val_ord_SEQE_0: |
|
754 assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')" |
|
755 shows "v1 \<sqsubset>val p v1'" |
|
756 using assms(1) |
|
757 apply(simp add: val_ord_def val_ord_ex_def) |
|
758 apply(auto)[1] |
|
759 apply(simp add: pflat_len_simps) |
|
760 apply(simp add: val_ord_def pflat_len_def) |
|
761 apply(auto)[1] |
|
762 apply(drule_tac x="0#q" in bspec) |
|
763 apply(simp) |
|
764 apply(simp) |
|
765 apply(drule_tac x="0#q" in bspec) |
|
766 apply(simp) |
|
767 apply(simp) |
|
768 apply(drule_tac x="0#q" in bspec) |
|
769 apply(simp) |
|
770 apply(simp) |
|
771 apply(simp add: val_ord_def pflat_len_def) |
|
772 apply(auto)[1] |
|
773 done |
|
774 |
|
775 lemma val_ord_SEQE_1: |
|
776 assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" |
|
777 shows "v2 \<sqsubset>val p v2'" |
|
778 using assms(1) |
|
779 apply(simp add: val_ord_def pflat_len_def) |
|
780 apply(auto)[1] |
|
781 apply(drule_tac x="1#q" in bspec) |
|
782 apply(simp) |
|
783 apply(simp) |
|
784 apply(drule_tac x="1#q" in bspec) |
|
785 apply(simp) |
|
786 apply(simp) |
|
787 apply(drule_tac x="1#q" in bspec) |
|
788 apply(simp) |
|
789 apply(auto)[1] |
|
790 apply(drule_tac x="1#q" in bspec) |
|
791 apply(simp) |
|
792 apply(auto) |
|
793 apply(simp add: intlen_append) |
|
794 apply force |
|
795 apply(simp add: intlen_append) |
|
796 apply force |
|
797 apply(simp add: intlen_append) |
|
798 apply force |
|
799 apply(simp add: intlen_append) |
|
800 apply force |
|
801 done |
|
802 |
|
803 lemma val_ord_SEQE_2: |
|
804 assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')" |
|
805 and "\<turnstile> v1 : r" "\<turnstile> v1' : r" |
|
806 shows "v1 = v1'" |
|
807 proof - |
|
808 have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0 # q \<sqsubset>lex 1#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q" |
|
809 using assms(1) |
|
810 apply(simp add: val_ord_def) |
|
811 apply(rule ballI) |
|
812 apply(clarify) |
|
813 apply(drule_tac x="0#q" in bspec) |
|
814 apply(auto)[1] |
|
815 apply(simp add: pflat_len_simps) |
|
816 done |
|
817 then have "Pos v1 = Pos v1'" |
|
818 apply(rule_tac Two_to_Three_orig) |
|
819 apply(rule ballI) |
|
820 apply(drule_tac x="pa" in bspec) |
|
821 apply(simp) |
|
822 apply(simp) |
|
823 done |
|
824 then show "v1 = v1'" |
|
825 apply(rule_tac Three_to_One) |
|
826 apply(rule assms) |
|
827 apply(rule assms) |
|
828 apply(simp) |
|
829 done |
|
830 qed |
|
831 |
|
832 lemma val_ord_SEQ: |
|
833 assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" |
|
834 and "flat (Seq v1 v2) = flat (Seq v1' v2')" |
|
835 and "\<turnstile> v1 : r" "\<turnstile> v1' : r" |
|
836 shows "(v1 :\<sqsubset>val v1') \<or> (v1 = v1' \<and> (v2 :\<sqsubset>val v2'))" |
|
837 using assms(1) |
|
838 apply(subst (asm) val_ord_ex_def) |
|
839 apply(erule exE) |
|
840 apply(simp only: val_ord_def) |
|
841 apply(simp) |
|
842 apply(erule conjE)+ |
|
843 apply(erule disjE) |
|
844 prefer 2 |
|
845 apply(erule disjE) |
|
846 apply(erule exE) |
|
847 apply(rule disjI1) |
|
848 apply(simp) |
|
849 apply(subst val_ord_ex_def) |
|
850 apply(rule_tac x="ps" in exI) |
|
851 apply(rule val_ord_SEQE_0) |
|
852 apply(simp add: val_ord_def) |
|
853 apply(erule exE) |
|
854 apply(rule disjI2) |
|
855 apply(rule conjI) |
|
856 thm val_ord_SEQE_1 |
|
857 apply(rule_tac val_ord_SEQE_2) |
|
858 apply(auto simp add: val_ord_def)[3] |
|
859 apply(rule assms(3)) |
|
860 apply(rule assms(4)) |
|
861 apply(subst val_ord_ex_def) |
|
862 apply(rule_tac x="ps" in exI) |
|
863 apply(rule_tac val_ord_SEQE_1) |
|
864 apply(auto simp add: val_ord_def)[1] |
|
865 apply(simp) |
|
866 using assms(2) |
|
867 apply(simp add: pflat_len_simps) |
|
868 done |
|
869 |
|
870 |
|
871 lemma val_ord_ex_trans: |
|
872 assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3" |
|
873 shows "v1 :\<sqsubset>val v3" |
|
874 using assms |
|
875 unfolding val_ord_ex_def |
|
876 apply(clarify) |
|
877 apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p") |
|
878 prefer 2 |
|
879 apply(rule trichotomous) |
|
880 apply(erule disjE) |
|
881 apply(simp) |
|
882 apply(rule_tac x="pa" in exI) |
|
883 apply(subst val_ord_def) |
|
884 apply(rule conjI) |
|
885 apply(simp add: val_ord_def) |
|
886 apply(auto)[1] |
|
887 apply(simp add: val_ord_def) |
|
888 apply(simp add: val_ord_def) |
|
889 apply(auto)[1] |
|
890 using outside_lemma apply blast |
|
891 apply(simp add: val_ord_def) |
|
892 apply(auto)[1] |
|
893 using outside_lemma apply force |
|
894 apply auto[1] |
|
895 apply(simp add: val_ord_def) |
|
896 apply(auto)[1] |
|
897 apply (metis (no_types, hide_lams) lex_trans outside_lemma) |
|
898 apply(simp add: val_ord_def) |
|
899 apply(auto)[1] |
|
900 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma) |
|
901 |
|
902 |
|
903 definition fdpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" |
|
904 where |
|
905 "fdpos v1 v2 p \<equiv> ({q. q \<sqsubset>lex p} \<inter> DPos v1 v2 = {})" |
|
906 |
|
907 |
|
908 lemma pos_append: |
|
909 assumes "p @ q \<in> Pos v" |
|
910 shows "q \<in> Pos (at v p)" |
|
911 using assms |
|
912 apply(induct arbitrary: p q rule: Pos.induct) |
|
913 apply(simp_all) |
|
914 apply(auto)[1] |
|
915 apply(simp add: append_eq_Cons_conv) |
|
916 apply(auto)[1] |
|
917 apply(auto)[1] |
|
918 apply(simp add: append_eq_Cons_conv) |
|
919 apply(auto)[1] |
|
920 apply(auto)[1] |
|
921 apply(simp add: append_eq_Cons_conv) |
|
922 apply(auto)[1] |
|
923 apply(simp add: append_eq_Cons_conv) |
|
924 apply(auto)[1] |
|
925 apply(auto)[1] |
|
926 apply(simp add: append_eq_Cons_conv) |
|
927 apply(auto)[1] |
|
928 apply(simp add: append_eq_Cons_conv) |
|
929 apply(auto)[1] |
|
930 by (metis append_Cons at.simps(6)) |
|
931 |
|
932 |
|
933 lemma Pos_pre: |
|
934 assumes "p \<in> Pos v" "q \<sqsubseteq>pre p" |
|
935 shows "q \<in> Pos v" |
|
936 using assms |
|
937 apply(induct v arbitrary: p q rule: Pos.induct) |
|
938 apply(simp_all add: prefix_list_def) |
|
939 apply (meson append_eq_Cons_conv append_is_Nil_conv) |
|
940 apply (meson append_eq_Cons_conv append_is_Nil_conv) |
|
941 apply (metis (no_types, lifting) Cons_eq_append_conv append_is_Nil_conv) |
|
942 apply(auto) |
|
943 apply (meson append_eq_Cons_conv) |
|
944 apply(simp add: append_eq_Cons_conv) |
|
945 apply(auto) |
|
946 done |
|
947 |
|
948 lemma lex_lists_order: |
|
949 assumes "q' \<sqsubset>lex q" "\<not>(q' \<sqsubseteq>pre q)" |
|
950 shows "\<not>(q \<sqsubset>lex q')" |
|
951 using assms |
|
952 apply(induct rule: lex_lists.induct) |
|
953 apply(simp add: prefix_list_def) |
|
954 apply(auto) |
|
955 using trichotomous_aux2 by auto |
|
956 |
|
957 lemma lex_appendL: |
|
958 assumes "q \<sqsubset>lex p" |
|
959 shows "q \<sqsubset>lex p @ q'" |
|
960 using assms |
|
961 apply(induct arbitrary: q' rule: lex_lists.induct) |
|
962 apply(auto) |
|
963 done |
|
964 |
|
965 |
|
966 inductive |
|
967 CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) |
|
968 where |
|
969 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
|
970 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
|
971 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
|
972 | "\<Turnstile> Void : ONE" |
|
973 | "\<Turnstile> Char c : CHAR c" |
|
974 | "\<Turnstile> Stars [] : STAR r" |
|
975 | "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r" |
|
976 |
|
977 lemma Prf_CPrf: |
|
978 assumes "\<Turnstile> v : r" |
|
979 shows "\<turnstile> v : r" |
|
980 using assms |
|
981 apply(induct) |
|
982 apply(auto intro: Prf.intros) |
|
983 done |
|
984 |
|
985 definition |
|
986 "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}" |
|
987 |
|
988 definition |
|
989 "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}" |
|
990 |
|
991 lemma CPT_CPTpre_subset: |
|
992 shows "CPT r s \<subseteq> CPTpre r s" |
|
993 apply(auto simp add: CPT_def CPTpre_def) |
|
994 done |
|
995 |
|
996 |
|
997 lemma CPTpre_subsets: |
|
998 "CPTpre ZERO s = {}" |
|
999 "CPTpre ONE s \<subseteq> {Void}" |
|
1000 "CPTpre (CHAR c) s \<subseteq> {Char c}" |
|
1001 "CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
1002 "CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" |
|
1003 "CPTpre (STAR r) s \<subseteq> {Stars []} \<union> |
|
1004 {Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}" |
|
1005 "CPTpre (STAR r) [] = {Stars []}" |
|
1006 apply(auto simp add: CPTpre_def) |
|
1007 apply(erule CPrf.cases) |
|
1008 apply(simp_all) |
|
1009 apply(erule CPrf.cases) |
|
1010 apply(simp_all) |
|
1011 apply(erule CPrf.cases) |
|
1012 apply(simp_all) |
|
1013 apply(erule CPrf.cases) |
|
1014 apply(simp_all) |
|
1015 apply(erule CPrf.cases) |
|
1016 apply(simp_all) |
|
1017 apply(erule CPrf.cases) |
|
1018 apply(simp_all) |
|
1019 apply(erule CPrf.cases) |
|
1020 apply(simp_all) |
|
1021 apply(rule CPrf.intros) |
|
1022 done |
|
1023 |
|
1024 |
|
1025 lemma CPTpre_simps: |
|
1026 shows "CPTpre ONE s = {Void}" |
|
1027 and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})" |
|
1028 and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
1029 and "CPTpre (SEQ r1 r2) s = |
|
1030 {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" |
|
1031 apply - |
|
1032 apply(rule subset_antisym) |
|
1033 apply(rule CPTpre_subsets) |
|
1034 apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1] |
|
1035 apply(case_tac "c = d") |
|
1036 apply(simp) |
|
1037 apply(rule subset_antisym) |
|
1038 apply(rule CPTpre_subsets) |
|
1039 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
1040 apply(simp) |
|
1041 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
1042 apply(erule CPrf.cases) |
|
1043 apply(simp_all) |
|
1044 apply(rule subset_antisym) |
|
1045 apply(rule CPTpre_subsets) |
|
1046 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
1047 apply(rule subset_antisym) |
|
1048 apply(rule CPTpre_subsets) |
|
1049 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
1050 done |
|
1051 |
|
1052 lemma CPT_simps: |
|
1053 shows "CPT ONE s = (if s = [] then {Void} else {})" |
|
1054 and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})" |
|
1055 and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s" |
|
1056 and "CPT (SEQ r1 r2) s = |
|
1057 {Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}" |
|
1058 apply - |
|
1059 apply(rule subset_antisym) |
|
1060 apply(auto simp add: CPT_def)[1] |
|
1061 apply(erule CPrf.cases) |
|
1062 apply(simp_all)[7] |
|
1063 apply(erule CPrf.cases) |
|
1064 apply(simp_all)[7] |
|
1065 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
1066 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
1067 apply(erule CPrf.cases) |
|
1068 apply(simp_all)[7] |
|
1069 apply(erule CPrf.cases) |
|
1070 apply(simp_all)[7] |
|
1071 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
1072 apply(erule CPrf.cases) |
|
1073 apply(simp_all)[7] |
|
1074 apply(clarify) |
|
1075 apply blast |
|
1076 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
1077 apply(erule CPrf.cases) |
|
1078 apply(simp_all)[7] |
|
1079 done |
|
1080 |
|
1081 lemma CPTpre_SEQ: |
|
1082 assumes "v \<in> CPTpre (SEQ r1 r2) s" |
|
1083 shows "\<exists>s'. flat v = s' \<and> (s' \<sqsubseteq>pre s) \<and> s' \<in> L (SEQ r1 r2)" |
|
1084 using assms |
|
1085 apply(simp add: CPTpre_simps) |
|
1086 apply(auto simp add: CPTpre_def) |
|
1087 apply (simp add: prefix_list_def) |
|
1088 by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5)) |
|
1089 |
|
1090 lemma Cond_prefix: |
|
1091 assumes "\<forall>s\<^sub>3. s1 @ s\<^sub>3 \<in> L r1 \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s1 @ s\<^sub>3 @ s\<^sub>4 \<sqsubseteq>pre s1 @ s2 \<longrightarrow> s\<^sub>4 \<notin> L r2)" |
|
1092 and "t1 \<in> L r1" "t2 \<in> L r2" "t1 @ t2 \<sqsubseteq>pre s1 @ s2" |
|
1093 shows "t1 \<sqsubseteq>pre s1" |
|
1094 using assms |
|
1095 apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2) |
|
1096 done |
|
1097 |
|
1098 |
|
1099 |
|
1100 lemma test: |
|
1101 assumes "finite A" |
|
1102 shows "finite {vs. Stars vs \<in> A}" |
|
1103 using assms |
|
1104 apply(induct A) |
|
1105 apply(simp) |
|
1106 apply(auto) |
|
1107 apply(case_tac x) |
|
1108 apply(simp_all) |
|
1109 done |
|
1110 |
|
1111 lemma CPTpre_STAR_finite: |
|
1112 assumes "\<And>s. finite (CPTpre r s)" |
|
1113 shows "finite (CPTpre (STAR r) s)" |
|
1114 apply(induct s rule: length_induct) |
|
1115 apply(case_tac xs) |
|
1116 apply(simp) |
|
1117 apply(simp add: CPTpre_subsets) |
|
1118 apply(rule finite_subset) |
|
1119 apply(rule CPTpre_subsets) |
|
1120 apply(simp) |
|
1121 apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset) |
|
1122 apply(auto)[1] |
|
1123 apply(rule finite_imageI) |
|
1124 apply(simp add: Collect_case_prod_Sigma) |
|
1125 apply(rule finite_SigmaI) |
|
1126 apply(rule assms) |
|
1127 apply(case_tac "flat v = []") |
|
1128 apply(simp) |
|
1129 apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) |
|
1130 apply(simp) |
|
1131 apply(auto)[1] |
|
1132 apply(rule test) |
|
1133 apply(simp) |
|
1134 done |
|
1135 |
|
1136 lemma CPTpre_finite: |
|
1137 shows "finite (CPTpre r s)" |
|
1138 apply(induct r arbitrary: s) |
|
1139 apply(simp add: CPTpre_subsets) |
|
1140 apply(rule finite_subset) |
|
1141 apply(rule CPTpre_subsets) |
|
1142 apply(simp) |
|
1143 apply(rule finite_subset) |
|
1144 apply(rule CPTpre_subsets) |
|
1145 apply(simp) |
|
1146 sorry |
|
1147 |
|
1148 |
|
1149 lemma CPT_finite: |
|
1150 shows "finite (CPT r s)" |
|
1151 apply(rule finite_subset) |
|
1152 apply(rule CPT_CPTpre_subset) |
|
1153 apply(rule CPTpre_finite) |
|
1154 done |
|
1155 |
|
1156 lemma Posix_CPT: |
|
1157 assumes "s \<in> r \<rightarrow> v" |
|
1158 shows "v \<in> CPT r s" |
|
1159 using assms |
|
1160 apply(induct rule: Posix.induct) |
|
1161 apply(simp add: CPT_def) |
|
1162 apply(rule CPrf.intros) |
|
1163 apply(simp add: CPT_def) |
|
1164 apply(rule CPrf.intros) |
|
1165 apply(simp add: CPT_def) |
|
1166 apply(rule CPrf.intros) |
|
1167 apply(simp) |
|
1168 apply(simp add: CPT_def) |
|
1169 apply(rule CPrf.intros) |
|
1170 apply(simp) |
|
1171 apply(simp add: CPT_def) |
|
1172 apply(rule CPrf.intros) |
|
1173 apply(simp) |
|
1174 apply(simp) |
|
1175 apply(simp add: CPT_def) |
|
1176 apply(rule CPrf.intros) |
|
1177 apply(simp) |
|
1178 apply(simp) |
|
1179 apply(simp) |
|
1180 apply(simp add: CPT_def) |
|
1181 apply(rule CPrf.intros) |
|
1182 done |
|
1183 |
|
1184 lemma Posix_val_ord: |
|
1185 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" |
|
1186 shows "v1 :\<sqsubseteq>val v2" |
|
1187 using assms |
|
1188 apply(induct arbitrary: v2 rule: Posix.induct) |
|
1189 apply(simp add: CPTpre_def) |
|
1190 apply(clarify) |
|
1191 apply(erule CPrf.cases) |
|
1192 apply(simp_all) |
|
1193 apply(simp add: val_ord_ex1_def) |
|
1194 apply(simp add: CPTpre_def) |
|
1195 apply(clarify) |
|
1196 apply(erule CPrf.cases) |
|
1197 apply(simp_all) |
|
1198 apply(simp add: val_ord_ex1_def) |
|
1199 (* ALT1 *) |
|
1200 prefer 3 |
|
1201 (* SEQ case *) |
|
1202 apply(subst (asm) (3) CPTpre_def) |
|
1203 apply(clarify) |
|
1204 apply(erule CPrf.cases) |
|
1205 apply(simp_all) |
|
1206 apply(case_tac "s' = []") |
|
1207 apply(simp) |
|
1208 prefer 2 |
|
1209 apply(simp add: val_ord_ex1_def) |
|
1210 apply(clarify) |
|
1211 apply(simp) |
|
1212 apply(simp add: val_ord_ex_def) |
|
1213 apply(simp (no_asm) add: val_ord_def) |
|
1214 apply(rule_tac x="[]" in exI) |
|
1215 apply(simp add: pflat_len_simps) |
|
1216 apply(rule intlen_length) |
|
1217 apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le) |
|
1218 apply(subgoal_tac "length (flat v1a) \<le> length s1") |
|
1219 prefer 2 |
|
1220 apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil) |
|
1221 apply(subst (asm) append_eq_append_conv_if) |
|
1222 apply(simp) |
|
1223 apply(clarify) |
|
1224 apply(drule_tac x="v1a" in meta_spec) |
|
1225 apply(drule meta_mp) |
|
1226 apply(auto simp add: CPTpre_def)[1] |
|
1227 using append_eq_conv_conj apply blast |
|
1228 apply(subst (asm) (2)val_ord_ex1_def) |
|
1229 apply(erule disjE) |
|
1230 apply(subst (asm) val_ord_ex_def) |
|
1231 apply(erule exE) |
|
1232 apply(subst val_ord_ex1_def) |
|
1233 apply(rule disjI1) |
|
1234 apply(subst val_ord_ex_def) |
|
1235 apply(rule_tac x="0#p" in exI) |
|
1236 apply(rule val_ord_SEQI) |
|
1237 apply(simp) |
|
1238 apply(simp) |
|
1239 apply (metis Posix1(2) append_assoc append_take_drop_id) |
|
1240 apply(simp) |
|
1241 apply(drule_tac x="v2b" in meta_spec) |
|
1242 apply(drule meta_mp) |
|
1243 apply(auto simp add: CPTpre_def)[1] |
|
1244 apply (simp add: Posix1(2)) |
|
1245 apply(subst (asm) val_ord_ex1_def) |
|
1246 apply(erule disjE) |
|
1247 apply(subst (asm) val_ord_ex_def) |
|
1248 apply(erule exE) |
|
1249 apply(subst val_ord_ex1_def) |
|
1250 apply(rule disjI1) |
|
1251 apply(subst val_ord_ex_def) |
|
1252 apply(rule_tac x="1#p" in exI) |
|
1253 apply(rule val_ord_SEQI2) |
|
1254 apply(simp) |
|
1255 apply (simp add: Posix1(2)) |
|
1256 apply(subst val_ord_ex1_def) |
|
1257 apply(simp) |
|
1258 (* ALT *) |
|
1259 apply(subst (asm) (2) CPTpre_def) |
|
1260 apply(clarify) |
|
1261 apply(erule CPrf.cases) |
|
1262 apply(simp_all) |
|
1263 apply(clarify) |
|
1264 apply(case_tac "s' = []") |
|
1265 apply(simp) |
|
1266 apply(drule_tac x="v1" in meta_spec) |
|
1267 apply(drule meta_mp) |
|
1268 apply(auto simp add: CPTpre_def)[1] |
|
1269 apply(subst (asm) val_ord_ex1_def) |
|
1270 apply(erule disjE) |
|
1271 apply(subst (asm) val_ord_ex_def) |
|
1272 apply(erule exE) |
|
1273 apply(subst val_ord_ex1_def) |
|
1274 apply(rule disjI1) |
|
1275 apply(subst val_ord_ex_def) |
|
1276 apply(rule_tac x="0#p" in exI) |
|
1277 apply(rule val_ord_ALTI) |
|
1278 apply(simp) |
|
1279 using Posix1(2) apply blast |
|
1280 using val_ord_ex1_def apply blast |
|
1281 apply(subst val_ord_ex1_def) |
|
1282 apply(rule disjI1) |
|
1283 apply (simp add: Posix1(2) val_ord_shorterI) |
|
1284 apply(subst val_ord_ex1_def) |
|
1285 apply(rule disjI1) |
|
1286 apply(case_tac "s' = []") |
|
1287 apply(simp) |
|
1288 apply(subst val_ord_ex_def) |
|
1289 apply(rule_tac x="[0]" in exI) |
|
1290 apply(subst val_ord_def) |
|
1291 apply(rule conjI) |
|
1292 apply(simp add: Pos_empty) |
|
1293 apply(rule conjI) |
|
1294 apply(simp add: pflat_len_simps) |
|
1295 apply (smt inlen_bigger) |
|
1296 apply(simp) |
|
1297 apply(rule conjI) |
|
1298 apply(simp add: pflat_len_simps) |
|
1299 using Posix1(2) apply auto[1] |
|
1300 apply(rule ballI) |
|
1301 apply(rule impI) |
|
1302 apply(case_tac "q = []") |
|
1303 using Posix1(2) apply auto[1] |
|
1304 apply(auto)[1] |
|
1305 apply(rule val_ord_shorterI) |
|
1306 apply(simp) |
|
1307 apply (simp add: Posix1(2)) |
|
1308 (* ALT RIGHT *) |
|
1309 apply(subst (asm) (2) CPTpre_def) |
|
1310 apply(clarify) |
|
1311 apply(erule CPrf.cases) |
|
1312 apply(simp_all) |
|
1313 apply(clarify) |
|
1314 apply(case_tac "s' = []") |
|
1315 apply(simp) |
|
1316 apply (simp add: L_flat_Prf1 Prf_CPrf) |
|
1317 apply(subst val_ord_ex1_def) |
|
1318 apply(rule disjI1) |
|
1319 apply(rule val_ord_shorterI) |
|
1320 apply(simp) |
|
1321 apply (simp add: Posix1(2)) |
|
1322 apply(case_tac "s' = []") |
|
1323 apply(simp) |
|
1324 apply(drule_tac x="v2a" in meta_spec) |
|
1325 apply(drule meta_mp) |
|
1326 apply(auto simp add: CPTpre_def)[1] |
|
1327 apply(subst (asm) val_ord_ex1_def) |
|
1328 apply(erule disjE) |
|
1329 apply(subst (asm) val_ord_ex_def) |
|
1330 apply(erule exE) |
|
1331 apply(subst val_ord_ex1_def) |
|
1332 apply(rule disjI1) |
|
1333 apply(subst val_ord_ex_def) |
|
1334 apply(rule_tac x="1#p" in exI) |
|
1335 apply(rule val_ord_ALTI2) |
|
1336 apply(simp) |
|
1337 using Posix1(2) apply blast |
|
1338 apply (simp add: val_ord_ex1_def) |
|
1339 apply(subst val_ord_ex1_def) |
|
1340 apply(rule disjI1) |
|
1341 apply(rule val_ord_shorterI) |
|
1342 apply(simp) |
|
1343 apply (simp add: Posix1(2)) |
|
1344 (* STAR empty case *) |
|
1345 prefer 2 |
|
1346 apply(subst (asm) CPTpre_def) |
|
1347 apply(clarify) |
|
1348 apply(erule CPrf.cases) |
|
1349 apply(simp_all) |
|
1350 apply(clarify) |
|
1351 apply (simp add: val_ord_ex1_def) |
|
1352 (* STAR non-empty case *) |
|
1353 apply(subst (asm) (3) CPTpre_def) |
|
1354 apply(clarify) |
|
1355 apply(erule CPrf.cases) |
|
1356 apply(simp_all) |
|
1357 apply(clarify) |
|
1358 apply (simp add: val_ord_ex1_def) |
|
1359 apply(rule val_ord_shorterI) |
|
1360 apply(simp) |
|
1361 apply(case_tac "s' = []") |
|
1362 apply(simp) |
|
1363 prefer 2 |
|
1364 apply (simp add: val_ord_ex1_def) |
|
1365 apply(rule disjI1) |
|
1366 apply(rule val_ord_shorterI) |
|
1367 apply(simp) |
|
1368 apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_all flat.simps(7) flat_Stars length_append not_less) |
|
1369 apply(drule_tac x="va" in meta_spec) |
|
1370 apply(drule meta_mp) |
|
1371 apply(auto simp add: CPTpre_def)[1] |
|
1372 apply (smt L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv2 flat_Stars self_append_conv) |
|
1373 apply (subst (asm) (2) val_ord_ex1_def) |
|
1374 apply(erule disjE) |
|
1375 prefer 2 |
|
1376 apply(simp) |
|
1377 apply(drule_tac x="Stars vsa" in meta_spec) |
|
1378 apply(drule meta_mp) |
|
1379 apply(auto simp add: CPTpre_def)[1] |
|
1380 apply (simp add: Posix1(2)) |
|
1381 apply (subst (asm) val_ord_ex1_def) |
|
1382 apply(erule disjE) |
|
1383 apply (subst (asm) val_ord_ex_def) |
|
1384 apply(erule exE) |
|
1385 apply (subst val_ord_ex1_def) |
|
1386 apply(rule disjI1) |
|
1387 apply (subst val_ord_ex_def) |
|
1388 apply(case_tac p) |
|
1389 apply(simp) |
|
1390 apply (metis Posix1(2) flat_Stars not_less_iff_gr_or_eq pflat_len_simps(7) same_append_eq val_ord_def) |
|
1391 using Posix1(2) val_ord_STARI2 apply fastforce |
|
1392 apply(simp add: val_ord_ex1_def) |
|
1393 apply (subst (asm) val_ord_ex_def) |
|
1394 apply(erule exE) |
|
1395 apply (subst val_ord_ex1_def) |
|
1396 apply(rule disjI1) |
|
1397 apply (subst val_ord_ex_def) |
|
1398 by (metis Posix1(2) flat.simps(7) flat_Stars val_ord_STARI) |
|
1399 |
|
1400 lemma Posix_val_ord_stronger: |
|
1401 assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s" |
|
1402 shows "v1 :\<sqsubseteq>val v2" |
|
1403 using assms |
|
1404 apply(rule_tac Posix_val_ord) |
|
1405 apply(assumption) |
|
1406 apply(simp add: CPTpre_def CPT_def) |
|
1407 done |
|
1408 |
|
1409 |
|
1410 lemma STAR_val_ord: |
|
1411 assumes "Stars (v1 # vs1) \<sqsubset>val (Suc p # ps) Stars (v2 # vs2)" "flat v1 = flat v2" |
|
1412 shows "(Stars vs1) \<sqsubset>val (p # ps) (Stars vs2)" |
|
1413 using assms(1,2) |
|
1414 apply - |
|
1415 apply(simp(no_asm) add: val_ord_def) |
|
1416 apply(rule conjI) |
|
1417 apply(simp add: val_ord_def) |
|
1418 apply(rule conjI) |
|
1419 apply(simp add: val_ord_def) |
|
1420 apply(auto simp add: pflat_len_simps pflat_len_Stars_simps2)[1] |
|
1421 apply(rule ballI) |
|
1422 apply(rule impI) |
|
1423 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1424 apply(clarify) |
|
1425 apply(case_tac q) |
|
1426 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1427 apply(clarify) |
|
1428 apply(erule disjE) |
|
1429 prefer 2 |
|
1430 apply(drule_tac x="Suc a # list" in bspec) |
|
1431 apply(simp) |
|
1432 apply(drule mp) |
|
1433 apply(simp) |
|
1434 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1435 apply(drule_tac x="Suc a # list" in bspec) |
|
1436 apply(simp) |
|
1437 apply(drule mp) |
|
1438 apply(simp) |
|
1439 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1440 done |
|
1441 |
|
1442 |
|
1443 lemma Posix_val_ord_reverse: |
|
1444 assumes "s \<in> r \<rightarrow> v1" |
|
1445 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
|
1446 using assms |
|
1447 by (metis Posix_val_ord_stronger less_irrefl val_ord_def |
|
1448 val_ord_ex1_def val_ord_ex_def val_ord_ex_trans) |
|
1449 |
|
1450 thm Posix.intros(6) |
|
1451 |
|
1452 inductive Prop :: "rexp \<Rightarrow> val list \<Rightarrow> bool" |
|
1453 where |
|
1454 "Prop r []" |
|
1455 | "\<lbrakk>Prop r vs; |
|
1456 \<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = concat (map flat vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
|
1457 \<Longrightarrow> Prop r (v # vs)" |
|
1458 |
|
1459 lemma STAR_val_ord_ex: |
|
1460 assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)" |
|
1461 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
1462 using assms |
|
1463 apply(subst (asm) val_ord_ex_def) |
|
1464 apply(erule exE) |
|
1465 apply(case_tac p) |
|
1466 apply(simp) |
|
1467 apply(simp add: val_ord_def pflat_len_simps intlen_append) |
|
1468 apply(subst val_ord_ex_def) |
|
1469 apply(rule_tac x="[]" in exI) |
|
1470 apply(simp add: val_ord_def pflat_len_simps Pos_empty) |
|
1471 apply(simp) |
|
1472 apply(case_tac a) |
|
1473 apply(clarify) |
|
1474 prefer 2 |
|
1475 using STAR_val_ord val_ord_ex_def apply blast |
|
1476 apply(auto simp add: pflat_len_Stars_simps2 val_ord_def pflat_len_def)[1] |
|
1477 done |
|
1478 |
|
1479 lemma STAR_val_ord_exI: |
|
1480 assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)" |
|
1481 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
1482 using assms |
|
1483 apply(induct vs) |
|
1484 apply(simp) |
|
1485 apply(simp) |
|
1486 apply(simp add: val_ord_ex_def) |
|
1487 apply(erule exE) |
|
1488 apply(case_tac p) |
|
1489 apply(simp) |
|
1490 apply(rule_tac x="[]" in exI) |
|
1491 apply(simp add: val_ord_def) |
|
1492 apply(auto simp add: pflat_len_simps intlen_append)[1] |
|
1493 apply(simp) |
|
1494 apply(rule_tac x="Suc aa#list" in exI) |
|
1495 apply(rule val_ord_STARI2) |
|
1496 apply(simp) |
|
1497 apply(simp) |
|
1498 done |
|
1499 |
|
1500 lemma STAR_val_ord_ex_append: |
|
1501 assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)" |
|
1502 shows "Stars vs1 :\<sqsubset>val Stars vs2" |
|
1503 using assms |
|
1504 apply(induct vs) |
|
1505 apply(simp) |
|
1506 apply(simp) |
|
1507 apply(drule STAR_val_ord_ex) |
|
1508 apply(simp) |
|
1509 done |
|
1510 |
|
1511 lemma STAR_val_ord_ex_append_eq: |
|
1512 assumes "flat (Stars vs1) = flat (Stars vs2)" |
|
1513 shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2" |
|
1514 using assms |
|
1515 apply(rule_tac iffI) |
|
1516 apply(erule STAR_val_ord_ex_append) |
|
1517 apply(rule STAR_val_ord_exI) |
|
1518 apply(auto) |
|
1519 done |
|
1520 |
|
1521 lemma Posix_STARI: |
|
1522 assumes "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> (flat v) \<in> r \<rightarrow> v" "Prop r vs" |
|
1523 shows "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" |
|
1524 using assms |
|
1525 apply(induct vs arbitrary: r) |
|
1526 apply(simp) |
|
1527 apply(rule Posix.intros) |
|
1528 apply(simp) |
|
1529 apply(rule Posix.intros) |
|
1530 apply(simp) |
|
1531 apply(auto)[1] |
|
1532 apply(erule Prop.cases) |
|
1533 apply(simp) |
|
1534 apply(simp) |
|
1535 apply(simp) |
|
1536 apply(erule Prop.cases) |
|
1537 apply(simp) |
|
1538 apply(auto)[1] |
|
1539 done |
|
1540 |
|
1541 lemma CPrf_stars: |
|
1542 assumes "\<Turnstile> Stars vs : STAR r" |
|
1543 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
|
1544 using assms |
|
1545 apply(induct vs) |
|
1546 apply(auto) |
|
1547 apply(erule CPrf.cases) |
|
1548 apply(simp_all) |
|
1549 apply(erule CPrf.cases) |
|
1550 apply(simp_all) |
|
1551 apply(erule CPrf.cases) |
|
1552 apply(simp_all) |
|
1553 apply(erule CPrf.cases) |
|
1554 apply(simp_all) |
|
1555 done |
|
1556 |
|
1557 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
1558 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
|
1559 |
|
1560 lemma exists: |
|
1561 assumes "s \<in> (L r)\<star>" |
|
1562 shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r" |
|
1563 using assms |
|
1564 apply(drule_tac Star_string) |
|
1565 apply(auto) |
|
1566 by (metis L_flat_Prf2 Prf_Stars Star_val) |
|
1567 |
|
1568 |
|
1569 lemma val_ord_Posix_Stars: |
|
1570 assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v" |
|
1571 and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))" |
|
1572 shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" |
|
1573 using assms |
|
1574 apply(induct vs) |
|
1575 apply(simp) |
|
1576 apply(rule Posix.intros) |
|
1577 apply(simp (no_asm)) |
|
1578 apply(rule Posix.intros) |
|
1579 apply(auto)[1] |
|
1580 apply(auto simp add: CPT_def PT_def)[1] |
|
1581 defer |
|
1582 apply(simp) |
|
1583 apply(drule meta_mp) |
|
1584 apply(auto simp add: CPT_def PT_def)[1] |
|
1585 apply(erule CPrf.cases) |
|
1586 apply(simp_all) |
|
1587 apply(drule meta_mp) |
|
1588 apply(auto simp add: CPT_def PT_def)[1] |
|
1589 apply(erule Prf.cases) |
|
1590 apply(simp_all) |
|
1591 apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_val_ord_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25)) |
|
1592 apply(clarify) |
|
1593 apply(drule_tac x="Stars (a#v#vsa)" in spec) |
|
1594 apply(simp) |
|
1595 apply(drule mp) |
|
1596 apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) |
|
1597 apply(subst (asm) (2) val_ord_ex_def) |
|
1598 apply(simp) |
|
1599 apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def) |
|
1600 apply(auto simp add: CPT_def PT_def)[1] |
|
1601 using CPrf_stars apply auto[1] |
|
1602 apply(auto)[1] |
|
1603 apply(auto simp add: CPT_def PT_def)[1] |
|
1604 apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r") |
|
1605 prefer 2 |
|
1606 apply (meson L_flat_Prf2) |
|
1607 apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)") |
|
1608 apply(clarify) |
|
1609 apply(drule_tac x="Stars (vA # vB)" in spec) |
|
1610 apply(simp) |
|
1611 apply(drule mp) |
|
1612 using Prf.intros(7) apply blast |
|
1613 apply(subst (asm) (2) val_ord_ex_def) |
|
1614 apply(simp) |
|
1615 prefer 2 |
|
1616 apply(simp) |
|
1617 using exists apply blast |
|
1618 prefer 2 |
|
1619 apply(drule meta_mp) |
|
1620 apply(erule CPrf.cases) |
|
1621 apply(simp_all) |
|
1622 apply(drule meta_mp) |
|
1623 apply(auto)[1] |
|
1624 prefer 2 |
|
1625 apply(simp) |
|
1626 apply(erule CPrf.cases) |
|
1627 apply(simp_all) |
|
1628 apply(clarify) |
|
1629 apply(rotate_tac 3) |
|
1630 apply(erule Prf.cases) |
|
1631 apply(simp_all) |
|
1632 apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def) |
|
1633 apply(drule_tac x="Stars (v#va#vsb)" in spec) |
|
1634 apply(drule mp) |
|
1635 apply (simp add: Posix1a Prf.intros(7)) |
|
1636 apply(simp) |
|
1637 apply(subst (asm) (2) val_ord_ex_def) |
|
1638 apply(simp) |
|
1639 apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def) |
|
1640 proof - |
|
1641 fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list" |
|
1642 assume a1: "s\<^sub>3 \<noteq> []" |
|
1643 assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)" |
|
1644 assume a3: "flat vA = flat a @ s\<^sub>3" |
|
1645 assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)" |
|
1646 have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs" |
|
1647 by (meson drop_eq_Nil not_less) |
|
1648 have f6: "\<not> length (flat vA) \<le> length (flat a)" |
|
1649 using a3 a1 by simp |
|
1650 have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))" |
|
1651 using a3 a2 by simp |
|
1652 then show False |
|
1653 using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_STARI val_ord_ex_def val_ord_shorterI) |
|
1654 qed |
|
1655 |
|
1656 lemma Prf_Stars_append: |
|
1657 assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r" |
|
1658 shows "\<turnstile> Stars (vs1 @ vs2) : STAR r" |
|
1659 using assms |
|
1660 apply(induct vs1 arbitrary: vs2) |
|
1661 apply(auto intro: Prf.intros) |
|
1662 apply(erule Prf.cases) |
|
1663 apply(simp_all) |
|
1664 apply(auto intro: Prf.intros) |
|
1665 done |
|
1666 |
|
1667 lemma CPrf_Stars_appendE: |
|
1668 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
1669 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
1670 using assms |
|
1671 apply(induct vs1 arbitrary: vs2) |
|
1672 apply(auto intro: CPrf.intros)[1] |
|
1673 apply(erule CPrf.cases) |
|
1674 apply(simp_all) |
|
1675 apply(auto intro: CPrf.intros) |
|
1676 done |
|
1677 |
|
1678 lemma val_ord_Posix: |
|
1679 assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)" |
|
1680 shows "s \<in> r \<rightarrow> v1" |
|
1681 using assms |
|
1682 apply(induct r arbitrary: s v1) |
|
1683 apply(auto simp add: CPT_def PT_def)[1] |
|
1684 apply(erule CPrf.cases) |
|
1685 apply(simp_all) |
|
1686 (* ONE *) |
|
1687 apply(auto simp add: CPT_def)[1] |
|
1688 apply(erule CPrf.cases) |
|
1689 apply(simp_all) |
|
1690 apply(rule Posix.intros) |
|
1691 (* CHAR *) |
|
1692 apply(auto simp add: CPT_def)[1] |
|
1693 apply(erule CPrf.cases) |
|
1694 apply(simp_all) |
|
1695 apply(rule Posix.intros) |
|
1696 prefer 2 |
|
1697 (* ALT *) |
|
1698 apply(auto simp add: CPT_def PT_def)[1] |
|
1699 apply(erule CPrf.cases) |
|
1700 apply(simp_all) |
|
1701 apply(rule Posix.intros) |
|
1702 apply(drule_tac x="flat v1a" in meta_spec) |
|
1703 apply(drule_tac x="v1a" in meta_spec) |
|
1704 apply(drule meta_mp) |
|
1705 apply(simp) |
|
1706 apply(drule meta_mp) |
|
1707 apply(auto)[1] |
|
1708 apply(drule_tac x="Left v2" in spec) |
|
1709 apply(simp) |
|
1710 apply(drule mp) |
|
1711 apply(rule Prf.intros) |
|
1712 apply(simp) |
|
1713 apply (meson val_ord_ALTI val_ord_ex_def) |
|
1714 apply(assumption) |
|
1715 (* ALT Right *) |
|
1716 apply(auto simp add: CPT_def)[1] |
|
1717 apply(rule Posix.intros) |
|
1718 apply(rotate_tac 1) |
|
1719 apply(drule_tac x="flat v2" in meta_spec) |
|
1720 apply(drule_tac x="v2" in meta_spec) |
|
1721 apply(drule meta_mp) |
|
1722 apply(simp) |
|
1723 apply(drule meta_mp) |
|
1724 apply(auto)[1] |
|
1725 apply(drule_tac x="Right v2a" in spec) |
|
1726 apply(simp) |
|
1727 apply(drule mp) |
|
1728 apply(rule Prf.intros) |
|
1729 apply(simp) |
|
1730 apply(subst (asm) (2) val_ord_ex_def) |
|
1731 apply(erule exE) |
|
1732 apply(drule val_ord_ALTI2) |
|
1733 apply(assumption) |
|
1734 apply(auto simp add: val_ord_ex_def)[1] |
|
1735 apply(assumption) |
|
1736 apply(auto)[1] |
|
1737 apply(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a") |
|
1738 apply(clarify) |
|
1739 apply(drule_tac x="Left v2'" in spec) |
|
1740 apply(simp) |
|
1741 apply(drule mp) |
|
1742 apply(rule Prf.intros) |
|
1743 apply(assumption) |
|
1744 apply(simp add: val_ord_ex_def) |
|
1745 apply(subst (asm) (3) val_ord_def) |
|
1746 apply(simp) |
|
1747 apply(simp add: pflat_len_simps) |
|
1748 apply(drule_tac x="[0]" in spec) |
|
1749 apply(simp add: pflat_len_simps Pos_empty) |
|
1750 apply(drule mp) |
|
1751 apply (smt inlen_bigger) |
|
1752 apply(erule disjE) |
|
1753 apply blast |
|
1754 apply auto[1] |
|
1755 apply (meson L_flat_Prf2) |
|
1756 (* SEQ *) |
|
1757 apply(auto simp add: CPT_def)[1] |
|
1758 apply(erule CPrf.cases) |
|
1759 apply(simp_all) |
|
1760 apply(rule Posix.intros) |
|
1761 apply(drule_tac x="flat v1a" in meta_spec) |
|
1762 apply(drule_tac x="v1a" in meta_spec) |
|
1763 apply(drule meta_mp) |
|
1764 apply(simp) |
|
1765 apply(drule meta_mp) |
|
1766 apply(auto)[1] |
|
1767 apply(auto simp add: PT_def)[1] |
|
1768 apply(drule_tac x="Seq v2a v2" in spec) |
|
1769 apply(simp) |
|
1770 apply(drule mp) |
|
1771 apply (simp add: Prf.intros(1) Prf_CPrf) |
|
1772 using val_ord_SEQI val_ord_ex_def apply fastforce |
|
1773 apply(assumption) |
|
1774 apply(rotate_tac 1) |
|
1775 apply(drule_tac x="flat v2" in meta_spec) |
|
1776 apply(drule_tac x="v2" in meta_spec) |
|
1777 apply(simp) |
|
1778 apply(auto)[1] |
|
1779 apply(drule meta_mp) |
|
1780 apply(auto)[1] |
|
1781 apply(auto simp add: PT_def)[1] |
|
1782 apply(drule_tac x="Seq v1a v2a" in spec) |
|
1783 apply(simp) |
|
1784 apply(drule mp) |
|
1785 apply (simp add: Prf.intros(1) Prf_CPrf) |
|
1786 apply (meson val_ord_SEQI2 val_ord_ex_def) |
|
1787 apply(assumption) |
|
1788 (* SEQ side condition *) |
|
1789 apply(auto simp add: PT_def) |
|
1790 apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a") |
|
1791 prefer 2 |
|
1792 apply (meson L_flat_Prf2) |
|
1793 apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a") |
|
1794 prefer 2 |
|
1795 apply (meson L_flat_Prf2) |
|
1796 apply(clarify) |
|
1797 apply(drule_tac x="Seq vA vB" in spec) |
|
1798 apply(simp) |
|
1799 apply(drule mp) |
|
1800 apply (simp add: Prf.intros(1)) |
|
1801 apply(subst (asm) (3) val_ord_ex_def) |
|
1802 apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SEQI val_ord_ex_def val_ord_shorterI) |
|
1803 (* STAR *) |
|
1804 apply(auto simp add: CPT_def)[1] |
|
1805 apply(erule CPrf.cases) |
|
1806 apply(simp_all)[6] |
|
1807 using Posix_STAR2 apply blast |
|
1808 apply(clarify) |
|
1809 apply(rule val_ord_Posix_Stars) |
|
1810 apply(auto simp add: CPT_def)[1] |
|
1811 apply (simp add: CPrf.intros(7)) |
|
1812 apply(auto)[1] |
|
1813 apply(drule_tac x="flat v" in meta_spec) |
|
1814 apply(drule_tac x="v" in meta_spec) |
|
1815 apply(simp) |
|
1816 apply(drule meta_mp) |
|
1817 apply(auto)[1] |
|
1818 apply(drule_tac x="Stars (v2#vs)" in spec) |
|
1819 apply(simp) |
|
1820 apply(drule mp) |
|
1821 using Prf.intros(7) Prf_CPrf apply blast |
|
1822 apply(subst (asm) (2) val_ord_ex_def) |
|
1823 apply(simp) |
|
1824 using val_ord_STARI val_ord_ex_def apply fastforce |
|
1825 apply(assumption) |
|
1826 apply(drule_tac x="flat va" in meta_spec) |
|
1827 apply(drule_tac x="va" in meta_spec) |
|
1828 apply(simp) |
|
1829 apply(drule meta_mp) |
|
1830 using CPrf_stars apply blast |
|
1831 apply(drule meta_mp) |
|
1832 apply(auto)[1] |
|
1833 apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post") |
|
1834 prefer 2 |
|
1835 apply (metis append_Cons append_Nil in_set_conv_decomp_first) |
|
1836 apply(clarify) |
|
1837 apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec) |
|
1838 apply(simp) |
|
1839 apply(drule mp) |
|
1840 apply(rule Prf.intros) |
|
1841 apply (simp add: Prf_CPrf) |
|
1842 apply(rule Prf_Stars_append) |
|
1843 apply(drule CPrf_Stars_appendE) |
|
1844 apply(auto simp add: Prf_CPrf)[1] |
|
1845 apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD) |
|
1846 apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)") |
|
1847 apply(subst (asm) STAR_val_ord_ex_append_eq) |
|
1848 apply(simp) |
|
1849 apply(subst (asm) STAR_val_ord_ex_append_eq) |
|
1850 apply(simp) |
|
1851 prefer 2 |
|
1852 apply(simp) |
|
1853 prefer 2 |
|
1854 apply(simp) |
|
1855 apply(simp add: val_ord_ex_def) |
|
1856 apply(erule exE) |
|
1857 apply(rotate_tac 6) |
|
1858 apply(drule_tac x="0#p" in spec) |
|
1859 apply (simp add: val_ord_STARI) |
|
1860 apply(auto simp add: PT_def) |
|
1861 done |
|
1862 |
8 |
1863 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100) |
9 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100) |
1864 where |
10 where |
1865 C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" |
11 C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" |
1866 | C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" |
12 | C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" |