equal
deleted
inserted
replaced
1 |
1 |
2 theory Re |
2 theory Re1 |
3 imports "Main" |
3 imports "Main" |
4 begin |
4 begin |
5 |
5 |
6 section {* Sequential Composition of Sets *} |
6 section {* Sequential Composition of Sets *} |
7 |
7 |
125 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
125 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
126 where |
126 where |
127 "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')" |
127 "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')" |
128 |
128 |
129 (* |
129 (* |
|
130 an alternative definition: might cause problems |
|
131 with theorem mkeps_POSIX |
|
132 *) |
|
133 |
|
134 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
|
135 where |
|
136 "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')" |
|
137 |
|
138 |
|
139 (* |
130 lemma POSIX_SEQ: |
140 lemma POSIX_SEQ: |
131 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
141 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
132 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
142 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
133 using assms |
143 using assms |
134 unfolding POSIX_def |
144 unfolding POSIX_def |
512 apply(simp_all) [5] |
522 apply(simp_all) [5] |
513 apply (metis ValOrd.intros(8)) |
523 apply (metis ValOrd.intros(8)) |
514 defer |
524 defer |
515 apply(auto) |
525 apply(auto) |
516 apply (metis POSIX_ALT_I1) |
526 apply (metis POSIX_ALT_I1) |
|
527 (* maybe it is too early to instantiate this existential quantifier *) |
|
528 (* potentially this is the wrong POSIX value *) |
517 apply(rule_tac x = "Seq v va" in exI ) |
529 apply(rule_tac x = "Seq v va" in exI ) |
518 apply(simp (no_asm) add: POSIX_def) |
530 apply(simp (no_asm) add: POSIX_def) |
519 apply(auto) |
531 apply(auto) |
520 apply(erule Prf.cases) |
532 apply(erule Prf.cases) |
521 apply(simp_all) |
533 apply(simp_all) |