44 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
44 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
45 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
45 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
46 | "\<Turnstile> Void : ONE" |
46 | "\<Turnstile> Void : ONE" |
47 | "\<Turnstile> Char c : CH c" |
47 | "\<Turnstile> Char c : CH c" |
48 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
48 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
|
49 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
|
50 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
|
51 length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n" |
49 |
52 |
50 inductive_cases Prf_elims: |
53 inductive_cases Prf_elims: |
51 "\<Turnstile> v : ZERO" |
54 "\<Turnstile> v : ZERO" |
52 "\<Turnstile> v : SEQ r1 r2" |
55 "\<Turnstile> v : SEQ r1 r2" |
53 "\<Turnstile> v : ALT r1 r2" |
56 "\<Turnstile> v : ALT r1 r2" |
54 "\<Turnstile> v : ONE" |
57 "\<Turnstile> v : ONE" |
55 "\<Turnstile> v : CH c" |
58 "\<Turnstile> v : CH c" |
56 "\<Turnstile> vs : STAR r" |
59 "\<Turnstile> vs : STAR r" |
|
60 "\<Turnstile> vs : NTIMES r n" |
57 |
61 |
58 lemma Prf_Stars_appendE: |
62 lemma Prf_Stars_appendE: |
59 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
63 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
60 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
64 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
61 using assms |
65 using assms |
62 by (auto intro: Prf.intros elim!: Prf_elims) |
66 by (auto intro: Prf.intros elim!: Prf_elims) |
63 |
67 |
|
68 lemma Pow_cstring: |
|
69 fixes A::"string set" |
|
70 assumes "s \<in> A ^^ n" |
|
71 shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> |
|
72 (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])" |
|
73 using assms |
|
74 apply(induct n arbitrary: s) |
|
75 apply(auto)[1] |
|
76 apply(auto simp add: Sequ_def) |
|
77 apply(drule_tac x="s2" in meta_spec) |
|
78 apply(simp) |
|
79 apply(erule exE)+ |
|
80 apply(clarify) |
|
81 apply(case_tac "s1 = []") |
|
82 apply(simp) |
|
83 apply(rule_tac x="ss1" in exI) |
|
84 apply(rule_tac x="s1 # ss2" in exI) |
|
85 apply(simp) |
|
86 apply(rule_tac x="s1 # ss1" in exI) |
|
87 apply(rule_tac x="ss2" in exI) |
|
88 apply(simp) |
|
89 done |
64 |
90 |
65 lemma flats_Prf_value: |
91 lemma flats_Prf_value: |
66 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
92 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
67 shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" |
93 shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" |
68 using assms |
94 using assms |
73 apply(case_tac "flat v = []") |
99 apply(case_tac "flat v = []") |
74 apply(rule_tac x="vs" in exI) |
100 apply(rule_tac x="vs" in exI) |
75 apply(simp) |
101 apply(simp) |
76 apply(rule_tac x="v#vs" in exI) |
102 apply(rule_tac x="v#vs" in exI) |
77 apply(simp) |
103 apply(simp) |
78 done |
104 done |
79 |
105 |
|
106 lemma Aux: |
|
107 assumes "\<forall>s\<in>set ss. s = []" |
|
108 shows "concat ss = []" |
|
109 using assms |
|
110 by (induct ss) (auto) |
|
111 |
|
112 lemma flats_cval: |
|
113 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
114 shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and> |
|
115 (\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []) \<and> |
|
116 (\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = [])" |
|
117 using assms |
|
118 apply(induct ss rule: rev_induct) |
|
119 apply(rule_tac x="[]" in exI)+ |
|
120 apply(simp) |
|
121 apply(simp) |
|
122 apply(clarify) |
|
123 apply(case_tac "flat v = []") |
|
124 apply(rule_tac x="vs1" in exI) |
|
125 apply(rule_tac x="v#vs2" in exI) |
|
126 apply(simp) |
|
127 apply(rule_tac x="vs1 @ [v]" in exI) |
|
128 apply(rule_tac x="vs2" in exI) |
|
129 apply(simp) |
|
130 by (simp add: Aux) |
|
131 |
|
132 lemma pow_Prf: |
|
133 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<in> A" |
|
134 shows "flats vs \<in> A ^^ (length vs)" |
|
135 using assms |
|
136 by (induct vs) (auto) |
80 |
137 |
81 lemma L_flat_Prf1: |
138 lemma L_flat_Prf1: |
82 assumes "\<Turnstile> v : r" |
139 assumes "\<Turnstile> v : r" |
83 shows "flat v \<in> L r" |
140 shows "flat v \<in> L r" |
84 using assms |
141 using assms |
85 by (induct) (auto simp add: Sequ_def Star_concat) |
142 apply (induct v r rule: Prf.induct) |
86 |
143 apply(auto simp add: Sequ_def Star_concat lang_pow_add) |
|
144 by (metis pow_Prf) |
|
145 |
87 lemma L_flat_Prf2: |
146 lemma L_flat_Prf2: |
88 assumes "s \<in> L r" |
147 assumes "s \<in> L r" |
89 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
148 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
90 using assms |
149 using assms |
91 proof(induct r arbitrary: s) |
150 proof(induct r arbitrary: s) |
103 then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s" |
162 then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s" |
104 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
163 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
105 next |
164 next |
106 case (ALT r1 r2 s) |
165 case (ALT r1 r2 s) |
107 then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s" |
166 then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s" |
108 unfolding L.simps by (fastforce intro: Prf.intros) |
167 unfolding L.simps by (fastforce intro: Prf.intros) |
|
168 next |
|
169 case (NTIMES r n) |
|
170 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
171 have "s \<in> L (NTIMES r n)" by fact |
|
172 then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n" |
|
173 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
|
174 using Pow_cstring by force |
|
175 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n" |
|
176 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
|
177 using IH flats_cval |
|
178 apply - |
|
179 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
|
180 apply(drule_tac x="r" in meta_spec) |
|
181 apply(drule meta_mp) |
|
182 apply(simp) |
|
183 apply (metis Un_iff) |
|
184 apply(clarify) |
|
185 apply(drule_tac x="vs1" in meta_spec) |
|
186 apply(drule_tac x="vs2" in meta_spec) |
|
187 apply(simp) |
|
188 done |
|
189 then show "\<exists>v. \<Turnstile> v : NTIMES r n \<and> flat v = s" |
|
190 using Prf.intros(7) flat_Stars by blast |
109 qed (auto intro: Prf.intros) |
191 qed (auto intro: Prf.intros) |
110 |
192 |
111 |
193 |
112 lemma L_flat_Prf: |
194 lemma L_flat_Prf: |
113 shows "L(r) = {flat v | v. \<Turnstile> v : r}" |
195 shows "L(r) = {flat v | v. \<Turnstile> v : r}" |
128 lemma LV_simps: |
210 lemma LV_simps: |
129 shows "LV ZERO s = {}" |
211 shows "LV ZERO s = {}" |
130 and "LV ONE s = (if s = [] then {Void} else {})" |
212 and "LV ONE s = (if s = [] then {Void} else {})" |
131 and "LV (CH c) s = (if s = [c] then {Char c} else {})" |
213 and "LV (CH c) s = (if s = [c] then {Char c} else {})" |
132 and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s" |
214 and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s" |
|
215 and "LV (NTIMES r 0) s = (if s = [] then {Stars []} else {})" |
133 unfolding LV_def |
216 unfolding LV_def |
134 by (auto intro: Prf.intros elim: Prf.cases) |
217 apply (auto intro: Prf.intros elim: Prf.cases) |
135 |
218 by (metis Prf.intros(7) append.right_neutral empty_iff list.set(1) list.size(3)) |
|
219 |
136 |
220 |
137 abbreviation |
221 abbreviation |
138 "Prefixes s \<equiv> {s'. prefix s' s}" |
222 "Prefixes s \<equiv> {s'. prefix s' s}" |
139 |
223 |
140 abbreviation |
224 abbreviation |
171 have "rev ` (Suffixes (rev s)) = Prefixes s" |
255 have "rev ` (Suffixes (rev s)) = Prefixes s" |
172 unfolding suffix_def prefix_def image_def |
256 unfolding suffix_def prefix_def image_def |
173 by (auto)(metis rev_append rev_rev_ident)+ |
257 by (auto)(metis rev_append rev_rev_ident)+ |
174 ultimately show "finite (Prefixes s)" by simp |
258 ultimately show "finite (Prefixes s)" by simp |
175 qed |
259 qed |
|
260 |
|
261 definition |
|
262 "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}" |
|
263 |
|
264 lemma finite_Stars_Append: |
|
265 assumes "finite Vs1" "finite Vs2" |
|
266 shows "finite (Stars_Append Vs1 Vs2)" |
|
267 using assms |
|
268 proof - |
|
269 define UVs1 where "UVs1 \<equiv> Stars -` Vs1" |
|
270 define UVs2 where "UVs2 \<equiv> Stars -` Vs2" |
|
271 from assms have "finite UVs1" "finite UVs2" |
|
272 unfolding UVs1_def UVs2_def |
|
273 by(simp_all add: finite_vimageI inj_on_def) |
|
274 then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))" |
|
275 by simp |
|
276 moreover |
|
277 have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)" |
|
278 unfolding Stars_Append_def UVs1_def UVs2_def by auto |
|
279 ultimately show "finite (Stars_Append Vs1 Vs2)" |
|
280 by simp |
|
281 qed |
|
282 |
|
283 lemma LV_NTIMES_subset: |
|
284 "LV (NTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) [])" |
|
285 apply(auto simp add: LV_def) |
|
286 apply(auto elim!: Prf_elims) |
|
287 apply(auto simp add: Stars_Append_def) |
|
288 apply(rule_tac x="vs1" in exI) |
|
289 apply(rule_tac x="vs2" in exI) |
|
290 apply(auto) |
|
291 using Prf.intros(6) apply(auto) |
|
292 apply(rule_tac x="length vs2" in bexI) |
|
293 thm Prf.intros |
|
294 apply(subst append.simps(1)[symmetric]) |
|
295 apply(rule Prf.intros) |
|
296 apply(auto)[1] |
|
297 apply(auto)[1] |
|
298 apply(simp) |
|
299 apply(simp) |
|
300 done |
|
301 |
|
302 lemma LV_NTIMES_Suc_empty: |
|
303 shows "LV (NTIMES r (Suc n)) [] = |
|
304 (\<lambda>(v, vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))" |
|
305 unfolding LV_def |
|
306 apply(auto elim!: Prf_elims simp add: image_def) |
|
307 apply(case_tac vs1) |
|
308 apply(auto) |
|
309 apply(case_tac vs2) |
|
310 apply(auto) |
|
311 apply(subst append.simps(1)[symmetric]) |
|
312 apply(rule Prf.intros) |
|
313 apply(auto) |
|
314 apply(subst append.simps(1)[symmetric]) |
|
315 apply(rule Prf.intros) |
|
316 apply(auto) |
|
317 done |
176 |
318 |
177 lemma LV_STAR_finite: |
319 lemma LV_STAR_finite: |
178 assumes "\<forall>s. finite (LV r s)" |
320 assumes "\<forall>s. finite (LV r s)" |
179 shows "finite (LV (STAR r) s)" |
321 shows "finite (LV (STAR r) s)" |
180 proof(induct s rule: length_induct) |
322 proof(induct s rule: length_induct) |
213 apply(simp add: suffix_def) |
355 apply(simp add: suffix_def) |
214 using Prf.intros(6) by blast |
356 using Prf.intros(6) by blast |
215 ultimately |
357 ultimately |
216 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
358 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
217 qed |
359 qed |
218 |
360 |
|
361 lemma finite_NTimes_empty: |
|
362 assumes "\<And>s. finite (LV r s)" |
|
363 shows "finite (LV (NTIMES r n) [])" |
|
364 using assms |
|
365 apply(induct n) |
|
366 apply(auto simp add: LV_simps) |
|
367 apply(subst LV_NTIMES_Suc_empty) |
|
368 apply(rule finite_imageI) |
|
369 apply(rule finite_cartesian_product) |
|
370 using assms apply simp |
|
371 apply(rule finite_vimageI) |
|
372 apply(simp) |
|
373 apply(simp add: inj_on_def) |
|
374 done |
|
375 |
219 |
376 |
220 lemma LV_finite: |
377 lemma LV_finite: |
221 shows "finite (LV r s)" |
378 shows "finite (LV r s)" |
222 proof(induct r arbitrary: s) |
379 proof(induct r arbitrary: s) |
223 case (ZERO s) |
380 case (ZERO s) |
249 show "finite (LV (SEQ r1 r2) s)" |
406 show "finite (LV (SEQ r1 r2) s)" |
250 by (simp add: finite_subset) |
407 by (simp add: finite_subset) |
251 next |
408 next |
252 case (STAR r s) |
409 case (STAR r s) |
253 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
410 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
|
411 next |
|
412 case (NTIMES r n s) |
|
413 have "\<And>s. finite (LV r s)" by fact |
|
414 then have "finite (Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) []))" |
|
415 apply(rule_tac finite_Stars_Append) |
|
416 apply (simp add: LV_STAR_finite) |
|
417 using finite_NTimes_empty by blast |
|
418 then show "finite (LV (NTIMES r n) s)" |
|
419 by (metis LV_NTIMES_subset finite_subset) |
254 qed |
420 qed |
255 |
421 |
256 |
422 |
257 |
423 |
258 section \<open>Our inductive POSIX Definition\<close> |
424 section \<open>Our inductive POSIX Definition\<close> |
269 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
435 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
270 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
436 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
271 \<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))\<rbrakk> |
437 \<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))\<rbrakk> |
272 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
438 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
273 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
439 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
|
440 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
|
441 \<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)))\<rbrakk> |
|
442 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r n \<rightarrow> Stars (v # vs)" |
|
443 | Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
|
444 \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs" |
274 |
445 |
275 inductive_cases Posix_elims: |
446 inductive_cases Posix_elims: |
276 "s \<in> ZERO \<rightarrow> v" |
447 "s \<in> ZERO \<rightarrow> v" |
277 "s \<in> ONE \<rightarrow> v" |
448 "s \<in> ONE \<rightarrow> v" |
278 "s \<in> CH c \<rightarrow> v" |
449 "s \<in> CH c \<rightarrow> v" |
279 "s \<in> ALT r1 r2 \<rightarrow> v" |
450 "s \<in> ALT r1 r2 \<rightarrow> v" |
280 "s \<in> SEQ r1 r2 \<rightarrow> v" |
451 "s \<in> SEQ r1 r2 \<rightarrow> v" |
281 "s \<in> STAR r \<rightarrow> v" |
452 "s \<in> STAR r \<rightarrow> v" |
|
453 "s \<in> NTIMES r n \<rightarrow> v" |
282 |
454 |
283 lemma Posix1: |
455 lemma Posix1: |
284 assumes "s \<in> r \<rightarrow> v" |
456 assumes "s \<in> r \<rightarrow> v" |
285 shows "s \<in> L r" "flat v = s" |
457 shows "s \<in> L r" "flat v = s" |
286 using assms |
458 using assms |
287 by(induct s r v rule: Posix.induct) |
459 apply(induct s r v rule: Posix.induct) |
288 (auto simp add: Sequ_def) |
460 apply(auto simp add: pow_empty_iff) |
|
461 apply (metis Suc_pred concI lang_pow.simps(2)) |
|
462 by (meson ex_in_conv set_empty) |
|
463 |
|
464 lemma Posix1a: |
|
465 assumes "s \<in> r \<rightarrow> v" |
|
466 shows "\<Turnstile> v : r" |
|
467 using assms |
|
468 apply(induct s r v rule: Posix.induct) |
|
469 apply(auto intro: Prf.intros) |
|
470 apply (metis Prf.intros(6) Prf_elims(6) set_ConsD val.inject(5)) |
|
471 prefer 2 |
|
472 apply (metis Posix1(2) Prf.intros(7) append_Nil empty_iff list.set(1)) |
|
473 apply(erule Prf_elims) |
|
474 apply(auto) |
|
475 apply(subst append.simps(2)[symmetric]) |
|
476 apply(rule Prf.intros) |
|
477 apply(auto) |
|
478 done |
289 |
479 |
290 text \<open> |
480 text \<open> |
291 For a give value and string, our Posix definition |
481 For a give value and string, our Posix definition |
292 determines a unique value. |
482 determines a unique value. |
293 \<close> |
483 \<close> |
|
484 |
|
485 lemma List_eq_zipI: |
|
486 assumes "list_all2 (\<lambda>v1 v2. v1 = v2) vs1 vs2" |
|
487 and "length vs1 = length vs2" |
|
488 shows "vs1 = vs2" |
|
489 using assms |
|
490 apply(induct vs1 vs2 rule: list_all2_induct) |
|
491 apply(auto) |
|
492 done |
294 |
493 |
295 lemma Posix_determ: |
494 lemma Posix_determ: |
296 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
495 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
297 shows "v1 = v2" |
496 shows "v1 = v2" |
298 using assms |
497 using assms |
354 ultimately show "Stars (v # vs) = v2" by auto |
553 ultimately show "Stars (v # vs) = v2" by auto |
355 next |
554 next |
356 case (Posix_STAR2 r v2) |
555 case (Posix_STAR2 r v2) |
357 have "[] \<in> STAR r \<rightarrow> v2" by fact |
556 have "[] \<in> STAR r \<rightarrow> v2" by fact |
358 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
557 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
558 next |
|
559 case (Posix_NTIMES2 vs r n v2) |
|
560 then show "Stars vs = v2" |
|
561 apply(erule_tac Posix_elims) |
|
562 apply(auto) |
|
563 apply (simp add: Posix1(2)) |
|
564 apply(rule List_eq_zipI) |
|
565 apply(auto simp add: list_all2_iff) |
|
566 by (meson in_set_zipE) |
|
567 next |
|
568 case (Posix_NTIMES1 s1 r v s2 n vs) |
|
569 have "(s1 @ s2) \<in> NTIMES r n \<rightarrow> v2" |
|
570 "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
571 "\<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+ |
|
572 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
|
573 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
574 using Posix1(1) apply fastforce |
|
575 apply (metis One_nat_def Posix1(1) Posix_NTIMES1.hyps(7) append.right_neutral append_self_conv2) |
|
576 using Posix1(2) by blast |
|
577 moreover |
|
578 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
579 "\<And>v2. s2 \<in> NTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
580 ultimately show "Stars (v # vs) = v2" by auto |
359 qed |
581 qed |
360 |
582 |
361 |
583 |
362 text \<open> |
584 text \<open> |
363 Our POSIX values are lexical values. |
585 Our POSIX values are lexical values. |
366 lemma Posix_LV: |
588 lemma Posix_LV: |
367 assumes "s \<in> r \<rightarrow> v" |
589 assumes "s \<in> r \<rightarrow> v" |
368 shows "v \<in> LV r s" |
590 shows "v \<in> LV r s" |
369 using assms unfolding LV_def |
591 using assms unfolding LV_def |
370 apply(induct rule: Posix.induct) |
592 apply(induct rule: Posix.induct) |
371 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) |
593 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a) |
372 done |
594 apply (smt (verit, best) One_nat_def Posix1a Posix_NTIMES1 L.simps(7)) |
373 |
595 using Posix1a Posix_NTIMES2 by blast |
374 lemma Posix_Prf: |
596 |
375 assumes "s \<in> r \<rightarrow> v" |
|
376 shows "\<Turnstile> v : r" |
|
377 using assms Posix_LV LV_def |
|
378 by simp |
|
379 |
597 |
380 end |
598 end |