70 | "flat(Char c) = [c]" |
70 | "flat(Char c) = [c]" |
71 | "flat(Left v) = flat(v)" |
71 | "flat(Left v) = flat(v)" |
72 | "flat(Right v) = flat(v)" |
72 | "flat(Right v) = flat(v)" |
73 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
73 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
74 |
74 |
|
75 fun flats :: "val \<Rightarrow> string list" |
|
76 where |
|
77 "flats(Void) = [[]]" |
|
78 | "flats(Char c) = [[c]]" |
|
79 | "flats(Left v) = flats(v)" |
|
80 | "flats(Right v) = flats(v)" |
|
81 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
75 |
82 |
76 lemma Prf_flat_L: |
83 lemma Prf_flat_L: |
77 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
84 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
78 using assms |
85 using assms |
79 apply(induct) |
86 apply(induct) |
91 apply (metis Prf.intros(3) flat.simps(4)) |
98 apply (metis Prf.intros(3) flat.simps(4)) |
92 apply(erule Prf.cases) |
99 apply(erule Prf.cases) |
93 apply(auto) |
100 apply(auto) |
94 done |
101 done |
95 |
102 |
|
103 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) |
|
104 where |
|
105 "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" |
|
106 |
96 section {* Ordering of values *} |
107 section {* Ordering of values *} |
97 |
108 |
98 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
109 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
99 where |
110 where |
100 "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
111 "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
104 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
115 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
105 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
116 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
106 | "Void \<succ>EMPTY Void" |
117 | "Void \<succ>EMPTY Void" |
107 | "(Char c) \<succ>(CHAR c) (Char c)" |
118 | "(Char c) \<succ>(CHAR c) (Char c)" |
108 |
119 |
109 (* |
120 section {* The ordering is reflexive *} |
110 lemma |
121 |
111 assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))" |
122 lemma ValOrd_refl: |
112 shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))" |
123 assumes "\<turnstile> v : r" |
113 using assms |
124 shows "v \<succ>r v" |
114 apply(simp) |
125 using assms |
115 apply(rule ValOrd.intros) |
126 apply(induct) |
116 apply(rule ValOrd.intros) |
127 apply(auto intro: ValOrd.intros) |
117 apply(rule ValOrd.intros) |
128 done |
118 apply(rule ValOrd.intros) |
129 |
119 apply(simp) |
130 lemma ValOrd_flats: |
120 done |
131 assumes "v1 \<succ>r v2" |
121 *) |
132 shows "hd (flats v2) = hd (flats v1)" |
|
133 using assms |
|
134 apply(induct) |
|
135 apply(auto) |
|
136 done |
|
137 |
122 |
138 |
123 section {* Posix definition *} |
139 section {* Posix definition *} |
124 |
140 |
125 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
141 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
126 where |
142 where |
138 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
154 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
139 where |
155 where |
140 "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')" |
156 "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')" |
141 |
157 |
142 |
158 |
143 (* |
|
144 lemma POSIX_SEQ: |
159 lemma POSIX_SEQ: |
145 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
160 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
146 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
161 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
147 using assms |
162 using assms |
148 unfolding POSIX_def |
163 unfolding POSIX_def |
149 apply(auto) |
164 apply(auto) |
150 apply(drule_tac x="Seq v' v2" in spec) |
165 apply(drule_tac x="Seq v' v2" in spec) |
151 apply(simp) |
166 apply(simp) |
152 apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
167 apply(erule impE) |
|
168 apply(rule Prf.intros) |
|
169 apply(simp) |
|
170 apply(simp) |
|
171 apply(erule ValOrd.cases) |
|
172 apply(simp_all) |
|
173 apply(clarify) |
|
174 defer |
153 apply(drule_tac x="Seq v1 v'" in spec) |
175 apply(drule_tac x="Seq v1 v'" in spec) |
154 apply(simp) |
176 apply(simp) |
155 by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
177 apply(erule impE) |
156 *) |
178 apply(rule Prf.intros) |
157 |
179 apply(simp) |
158 (* |
180 apply(simp) |
|
181 apply(erule ValOrd.cases) |
|
182 apply(simp_all) |
|
183 apply(clarify) |
|
184 oops (*not true*) |
|
185 |
159 lemma POSIX_SEQ_I: |
186 lemma POSIX_SEQ_I: |
160 assumes "POSIX v1 r1" "POSIX v2 r2" |
187 assumes "POSIX v1 r1" "POSIX v2 r2" |
161 shows "POSIX (Seq v1 v2) (SEQ r1 r2)" |
188 shows "POSIX (Seq v1 v2) (SEQ r1 r2)" |
162 using assms |
189 using assms |
163 unfolding POSIX_def |
190 unfolding POSIX_def |
165 apply(rotate_tac 2) |
192 apply(rotate_tac 2) |
166 apply(erule Prf.cases) |
193 apply(erule Prf.cases) |
167 apply(simp_all)[5] |
194 apply(simp_all)[5] |
168 apply(auto)[1] |
195 apply(auto)[1] |
169 apply(rule ValOrd.intros) |
196 apply(rule ValOrd.intros) |
170 |
197 oops (* maybe also not true *) |
171 apply(auto) |
198 |
172 done |
199 lemma POSIX3_SEQ_I: |
173 *) |
200 assumes "POSIX3 v1 r1" "POSIX3 v2 r2" |
174 |
201 shows "POSIX3 (Seq v1 v2) (SEQ r1 r2)" |
175 |
202 using assms |
176 |
203 unfolding POSIX3_def |
|
204 apply(auto) |
|
205 apply (metis Prf.intros(1)) |
|
206 apply(rotate_tac 4) |
|
207 apply(erule Prf.cases) |
|
208 apply(simp_all)[5] |
|
209 apply(auto)[1] |
|
210 apply(case_tac "v1 = v1a") |
|
211 apply(auto) |
|
212 apply (metis ValOrd.intros(1)) |
|
213 apply (rule ValOrd.intros(2)) |
177 |
214 |
178 lemma POSIX_ALT2: |
215 lemma POSIX_ALT2: |
179 assumes "POSIX (Left v1) (ALT r1 r2)" |
216 assumes "POSIX (Left v1) (ALT r1 r2)" |
180 shows "POSIX v1 r1" |
217 shows "POSIX v1 r1" |
181 using assms |
218 using assms |
377 using assms |
406 using assms |
378 apply(induct r) |
407 apply(induct r) |
379 apply(auto)[1] |
408 apply(auto)[1] |
380 apply(simp add: POSIX2_def) |
409 apply(simp add: POSIX2_def) |
381 oops |
410 oops |
|
411 |
|
412 lemma mkeps_POSIX3: |
|
413 assumes "nullable r" |
|
414 shows "POSIX3 (mkeps r) r" |
|
415 using assms |
|
416 apply(induct r) |
|
417 apply(auto)[1] |
|
418 apply(simp add: POSIX3_def) |
|
419 apply(auto)[1] |
|
420 apply (metis Prf.intros(4)) |
|
421 apply(erule Prf.cases) |
|
422 apply(simp_all)[5] |
|
423 apply (metis ValOrd.intros) |
|
424 apply(simp add: POSIX3_def) |
|
425 apply(auto)[1] |
|
426 apply(simp add: POSIX3_def) |
|
427 apply(auto)[1] |
|
428 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5)) |
|
429 apply(rotate_tac 6) |
|
430 apply(erule Prf.cases) |
|
431 apply(simp_all)[5] |
|
432 apply (metis ValOrd.intros(2) add_leE gen_length_code(1) gen_length_def mkeps_flat) |
|
433 apply(auto) |
|
434 apply(simp add: POSIX3_def) |
|
435 apply(auto) |
|
436 apply (metis Prf.intros(2)) |
|
437 apply(rotate_tac 4) |
|
438 apply(erule Prf.cases) |
|
439 apply(simp_all)[5] |
|
440 apply (metis ValOrd.intros(6)) |
|
441 apply(auto)[1] |
|
442 apply (metis ValOrd.intros(3)) |
|
443 apply(simp add: POSIX3_def) |
|
444 apply(auto) |
|
445 apply (metis Prf.intros(2)) |
|
446 apply(rotate_tac 6) |
|
447 apply(erule Prf.cases) |
|
448 apply(simp_all)[5] |
|
449 apply (metis ValOrd.intros(6)) |
|
450 apply (metis ValOrd.intros(3)) |
|
451 apply(simp add: POSIX3_def) |
|
452 apply(auto) |
|
453 apply (metis Prf.intros(3)) |
|
454 apply(rotate_tac 5) |
|
455 apply(erule Prf.cases) |
|
456 apply(simp_all)[5] |
|
457 apply (metis Prf_flat_L drop_0 drop_all list.size(3) mkeps_flat nullable_correctness) |
|
458 by (metis ValOrd.intros(5)) |
|
459 |
382 |
460 |
383 lemma mkeps_POSIX: |
461 lemma mkeps_POSIX: |
384 assumes "nullable r" |
462 assumes "nullable r" |
385 shows "POSIX (mkeps r) r" |
463 shows "POSIX (mkeps r) r" |
386 using assms |
464 using assms |
633 apply(simp_all)[5] |
711 apply(simp_all)[5] |
634 apply(auto)[1] |
712 apply(auto)[1] |
635 apply(simp add: v4) |
713 apply(simp add: v4) |
636 done |
714 done |
637 |
715 |
|
716 lemma "L r \<noteq> {} \<Longrightarrow> \<exists>v. POSIX3 v r" |
|
717 apply(induct r) |
|
718 apply(simp) |
|
719 apply(simp add: POSIX3_def) |
|
720 apply(rule_tac x="Void" in exI) |
|
721 apply(auto)[1] |
|
722 apply (metis Prf.intros(4)) |
|
723 apply (metis POSIX3_def flat.simps(1) mkeps.simps(1) mkeps_POSIX3 nullable.simps(2) order_refl) |
|
724 apply(simp add: POSIX3_def) |
|
725 apply(rule_tac x="Char char" in exI) |
|
726 apply(auto)[1] |
|
727 apply (metis Prf.intros(5)) |
|
728 apply(erule Prf.cases) |
|
729 apply(simp_all)[5] |
|
730 apply (metis ValOrd.intros(8)) |
|
731 apply(simp add: Sequ_def) |
|
732 apply(auto)[1] |
|
733 apply(drule meta_mp) |
|
734 apply(auto)[2] |
|
735 apply(drule meta_mp) |
|
736 apply(auto)[2] |
|
737 apply(rule_tac x="Seq v va" in exI) |
|
738 apply(simp (no_asm) add: POSIX3_def) |
|
739 apply(auto)[1] |
|
740 apply (metis POSIX3_def Prf.intros(1)) |
|
741 apply(erule Prf.cases) |
|
742 apply(simp_all)[5] |
|
743 apply(clarify) |
|
744 apply(case_tac "v \<succ>r1a v1") |
|
745 apply(rule ValOrd.intros(2)) |
|
746 apply(simp) |
|
747 apply(case_tac "v = v1") |
|
748 apply(rule ValOrd.intros(1)) |
|
749 apply(simp) |
|
750 apply(simp) |
|
751 apply (metis ValOrd_refl) |
|
752 apply(simp add: POSIX3_def) |
|
753 |
|
754 |
638 lemma "\<exists>v. POSIX v r" |
755 lemma "\<exists>v. POSIX v r" |
639 apply(induct r) |
756 apply(induct r) |
640 apply(rule exI) |
757 apply(rule exI) |
641 apply(simp add: POSIX_def) |
758 apply(simp add: POSIX_def) |
642 apply (metis (full_types) Prf_flat_L der.simps(1) der.simps(2) der.simps(3) flat.simps(1) nullable.simps(1) nullable_correctness proj_inj_id projval.simps(1) v3 v4) |
759 apply (metis (full_types) Prf_flat_L der.simps(1) der.simps(2) der.simps(3) flat.simps(1) nullable.simps(1) nullable_correctness proj_inj_id projval.simps(1) v3 v4) |
682 apply(auto)[1] |
799 apply(auto)[1] |
683 apply(rule ValOrd.intros(2)) |
800 apply(rule ValOrd.intros(2)) |
684 apply(rule ValOrd.intros) |
801 apply(rule ValOrd.intros) |
685 apply(case_tac "\<exists>r1a r1b. r1 = ALT r1a r1b") |
802 apply(case_tac "\<exists>r1a r1b. r1 = ALT r1a r1b") |
686 apply(auto) |
803 apply(auto) |
687 apply(rule_tac x = "Seq () va" in exI ) |
804 oops (* not sure if this can be proved by induction *) |
688 apply(simp (no_asm) add: POSIX_def) |
|
689 apply(auto) |
|
690 apply(erule Prf.cases) |
|
691 apply(simp_all) |
|
692 apply(auto)[1] |
|
693 apply(erule Prf.cases) |
|
694 apply(simp_all) |
|
695 apply(auto)[1] |
|
696 apply(rule ValOrd.intros(2)) |
|
697 apply(rule ValOrd.intros) |
|
698 |
|
699 apply(case_tac "v \<succ>r1a v1") |
|
700 apply (metis ValOrd.intros(2)) |
|
701 apply(simp add: POSIX_def) |
|
702 apply(case_tac "flat v = flat v1") |
|
703 apply(auto)[1] |
|
704 apply(simp only: append_eq_append_conv2) |
|
705 apply(auto) |
|
706 thm append_eq_append_conv2 |
|
707 |
805 |
708 text {* |
806 text {* |
709 |
807 |
710 HERE: Crucial lemma that does not go through in the sequence case. |
808 HERE: Crucial lemma that does not go through in the sequence case. |
711 |
809 |
740 apply(clarify) |
838 apply(clarify) |
741 apply(subgoal_tac "POSIX v2 (der c r2)") |
839 apply(subgoal_tac "POSIX v2 (der c r2)") |
742 prefer 2 |
840 prefer 2 |
743 apply(auto simp add: POSIX_def)[1] |
841 apply(auto simp add: POSIX_def)[1] |
744 apply (metis POSIX_ALT1a POSIX_def flat.simps(4)) |
842 apply (metis POSIX_ALT1a POSIX_def flat.simps(4)) |
|
843 apply(frule POSIX_ALT1a) |
|
844 apply(drule POSIX_ALT1b) |
|
845 apply(rule POSIX_ALT_I2) |
745 apply(rotate_tac 1) |
846 apply(rotate_tac 1) |
746 apply(drule_tac x="v2" in meta_spec) |
847 apply(drule_tac x="v2" in meta_spec) |
747 apply(simp) |
848 apply(simp) |
748 apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)") |
849 apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)") |
749 prefer 2 |
850 prefer 2 |
750 apply (metis Prf.intros(3) v3) |
851 apply (metis Prf.intros(3) v3) |
|
852 |
|
853 apply auto[1] |
|
854 apply(subst v4) |
|
855 apply(auto)[2] |
|
856 apply(subst (asm) (4) POSIX_def) |
|
857 apply(subst (asm) v4) |
|
858 apply(drule_tac x="v2" in meta_spec) |
|
859 apply(simp) |
|
860 |
|
861 apply(auto)[2] |
|
862 |
|
863 thm POSIX_ALT_I2 |
|
864 apply(rule POSIX_ALT_I2) |
|
865 |
751 apply(rule ccontr) |
866 apply(rule ccontr) |
752 apply(auto simp add: POSIX_def)[1] |
867 apply(auto simp add: POSIX_def)[1] |
753 |
868 |
754 apply(rule allI) |
869 apply(rule allI) |
755 apply(rule impI) |
870 apply(rule impI) |