equal
deleted
inserted
replaced
393 ultimately |
393 ultimately |
394 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
394 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
395 moreover |
395 moreover |
396 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
396 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
397 unfolding S1_def S2_def f_def |
397 unfolding S1_def S2_def f_def |
398 unfolding LV_def image_def prefix_def strict_suffix_def |
398 unfolding LV_def image_def prefix_def strict_suffix_def |
399 apply(auto) |
399 apply(auto) |
400 apply(case_tac x) |
400 apply(case_tac x) |
401 apply(auto elim: Prf_elims) |
401 apply(auto elim: Prf_elims) |
402 apply(erule Prf_elims) |
402 apply(erule Prf_elims) |
403 apply(auto) |
403 apply(auto) |
557 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
557 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
558 qed |
558 qed |
559 |
559 |
560 |
560 |
561 text {* |
561 text {* |
562 Our POSIX value is a lexical value. |
562 Our POSIX values are lexical values. |
563 *} |
563 *} |
564 |
564 |
565 lemma Posix_LV: |
565 lemma Posix_LV: |
566 assumes "s \<in> r \<rightarrow> v" |
566 assumes "s \<in> r \<rightarrow> v" |
567 shows "v \<in> LV r s" |
567 shows "v \<in> LV r s" |
568 using assms unfolding LV_def |
568 using assms unfolding LV_def |
569 apply(induct rule: Posix.induct) |
569 apply(induct rule: Posix.induct) |
570 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) |
570 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) |
571 done |
571 done |
572 |
572 |
|
573 lemma Posix_Prf: |
|
574 assumes "s \<in> r \<rightarrow> v" |
|
575 shows "\<Turnstile> v : r" |
|
576 using assms Posix_LV LV_def |
|
577 by simp |
573 |
578 |
574 end |
579 end |