209 | "\<Turnstile> Void : EMPTY" |
209 | "\<Turnstile> Void : EMPTY" |
210 | "\<Turnstile> Char c : CHAR c" |
210 | "\<Turnstile> Char c : CHAR c" |
211 | "\<Turnstile> Star [] : STAR r" |
211 | "\<Turnstile> Star [] : STAR r" |
212 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Star vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Star (v # vs) : STAR r" |
212 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Star vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Star (v # vs) : STAR r" |
213 |
213 |
214 |
|
215 inductive |
214 inductive |
216 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
215 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
217 where |
216 where |
218 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
217 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
219 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
218 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
229 using assms |
228 using assms |
230 apply(induct) |
229 apply(induct) |
231 apply(auto intro: Prf.intros) |
230 apply(auto intro: Prf.intros) |
232 done |
231 done |
233 |
232 |
|
233 lemma NPrf_Prf_val: |
|
234 shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r" |
|
235 and "\<turnstile> Star vs : r \<Longrightarrow> \<exists>vs'. flat (Star vs') = flat (Star vs) \<and> \<Turnstile> Star vs' : r" |
|
236 using assms |
|
237 apply(induct v and vs arbitrary: r and r rule: val.inducts) |
|
238 apply(auto)[1] |
|
239 apply(erule Prf.cases) |
|
240 apply(simp_all)[7] |
|
241 apply(rule_tac x="Void" in exI) |
|
242 apply(simp) |
|
243 apply(rule NPrf.intros) |
|
244 apply(erule Prf.cases) |
|
245 apply(simp_all)[7] |
|
246 apply(rule_tac x="Char c" in exI) |
|
247 apply(simp) |
|
248 apply(rule NPrf.intros) |
|
249 apply(erule Prf.cases) |
|
250 apply(simp_all)[7] |
|
251 apply(auto)[1] |
|
252 apply(drule_tac x="r1" in meta_spec) |
|
253 apply(drule_tac x="r2" in meta_spec) |
|
254 apply(simp) |
|
255 apply(auto)[1] |
|
256 apply(rule_tac x="Seq v' v'a" in exI) |
|
257 apply(simp) |
|
258 apply (metis NPrf.intros(1)) |
|
259 apply(erule Prf.cases) |
|
260 apply(simp_all)[7] |
|
261 apply(clarify) |
|
262 apply(drule_tac x="r2" in meta_spec) |
|
263 apply(simp) |
|
264 apply(auto)[1] |
|
265 apply(rule_tac x="Right v'" in exI) |
|
266 apply(simp) |
|
267 apply (metis NPrf.intros) |
|
268 apply(erule Prf.cases) |
|
269 apply(simp_all)[7] |
|
270 apply(clarify) |
|
271 apply(drule_tac x="r1" in meta_spec) |
|
272 apply(simp) |
|
273 apply(auto)[1] |
|
274 apply(rule_tac x="Left v'" in exI) |
|
275 apply(simp) |
|
276 apply (metis NPrf.intros) |
|
277 apply(drule_tac x="r" in meta_spec) |
|
278 apply(simp) |
|
279 apply(auto)[1] |
|
280 apply(rule_tac x="Star vs'" in exI) |
|
281 apply(simp) |
|
282 apply(rule_tac x="[]" in exI) |
|
283 apply(simp) |
|
284 apply(erule Prf.cases) |
|
285 apply(simp_all)[7] |
|
286 apply (metis NPrf.intros(6)) |
|
287 apply(erule Prf.cases) |
|
288 apply(simp_all)[7] |
|
289 apply(auto)[1] |
|
290 apply(drule_tac x="ra" in meta_spec) |
|
291 apply(simp) |
|
292 apply(drule_tac x="STAR ra" in meta_spec) |
|
293 apply(simp) |
|
294 apply(auto) |
|
295 apply(case_tac "flat v = []") |
|
296 apply(rule_tac x="vs'" in exI) |
|
297 apply(simp) |
|
298 apply(rule_tac x="v' # vs'" in exI) |
|
299 apply(simp) |
|
300 apply(rule NPrf.intros) |
|
301 apply(auto) |
|
302 done |
|
303 |
|
304 lemma NPrf_Prf: |
|
305 shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}" |
|
306 apply(auto) |
|
307 apply (metis NPrf_Prf_val(1)) |
|
308 by (metis NPrf_imp_Prf) |
|
309 |
|
310 |
234 lemma not_nullable_flat: |
311 lemma not_nullable_flat: |
235 assumes "\<turnstile> v : r" "\<not>nullable r" |
312 assumes "\<turnstile> v : r" "\<not>nullable r" |
236 shows "flat v \<noteq> []" |
313 shows "flat v \<noteq> []" |
237 using assms |
314 using assms |
238 apply(induct) |
315 apply(induct) |
244 using assms |
321 using assms |
245 apply(induct v r rule: Prf.induct) |
322 apply(induct v r rule: Prf.induct) |
246 apply(auto simp add: Sequ_def) |
323 apply(auto simp add: Sequ_def) |
247 done |
324 done |
248 |
325 |
|
326 lemma NPrf_flat_L: |
|
327 assumes "\<Turnstile> v : r" shows "flat v \<in> L r" |
|
328 using assms |
|
329 by (metis NPrf_imp_Prf Prf_flat_L) |
|
330 |
249 lemma Prf_Star: |
331 lemma Prf_Star: |
250 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
332 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
251 shows "\<turnstile> Star vs : STAR r" |
333 shows "\<turnstile> Star vs : STAR r" |
252 using assms |
334 using assms |
253 apply(induct vs) |
335 apply(induct vs) |
267 done |
349 done |
268 |
350 |
269 lemma Star_val: |
351 lemma Star_val: |
270 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
352 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
271 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
353 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
354 using assms |
|
355 apply(induct ss) |
|
356 apply(auto) |
|
357 apply (metis empty_iff list.set(1)) |
|
358 by (metis concat.simps(2) list.simps(9) set_ConsD) |
|
359 |
|
360 lemma Star_valN: |
|
361 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
362 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r)" |
272 using assms |
363 using assms |
273 apply(induct ss) |
364 apply(induct ss) |
274 apply(auto) |
365 apply(auto) |
275 apply (metis empty_iff list.set(1)) |
366 apply (metis empty_iff list.set(1)) |
276 by (metis concat.simps(2) list.simps(9) set_ConsD) |
367 by (metis concat.simps(2) list.simps(9) set_ConsD) |
295 apply(drule Star_string) |
386 apply(drule Star_string) |
296 apply(auto) |
387 apply(auto) |
297 apply(rule Star_val) |
388 apply(rule Star_val) |
298 apply(simp) |
389 apply(simp) |
299 done |
390 done |
|
391 |
|
392 lemma L_flat_NPrf: |
|
393 "L(r) = {flat v | v. \<Turnstile> v : r}" |
|
394 by (metis L_flat_Prf NPrf_Prf) |
|
395 |
|
396 text {* nicer proofs by Fahad *} |
300 |
397 |
301 lemma Prf_Star_flat_L: |
398 lemma Prf_Star_flat_L: |
302 assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>" |
399 assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>" |
303 using assms |
400 using assms |
304 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct) |
401 apply(induct v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct) |
611 apply(simp_all)[7] |
708 apply(simp_all)[7] |
612 apply(auto) |
709 apply(auto) |
613 apply (metis Prf.intros(6) Prf.intros(7)) |
710 apply (metis Prf.intros(6) Prf.intros(7)) |
614 by (metis Prf.intros(7)) |
711 by (metis Prf.intros(7)) |
615 |
712 |
616 lemma v3_NP: |
|
617 assumes "\<Turnstile> v : der c r" |
|
618 shows "\<Turnstile> (injval r c v) : r" |
|
619 using assms |
|
620 apply(induct arbitrary: v rule: der.induct) |
|
621 apply(simp) |
|
622 apply(erule NPrf.cases) |
|
623 apply(simp_all)[7] |
|
624 apply(simp) |
|
625 apply(erule NPrf.cases) |
|
626 apply(simp_all)[7] |
|
627 apply(case_tac "c = c'") |
|
628 apply(simp) |
|
629 apply(erule NPrf.cases) |
|
630 apply(simp_all)[7] |
|
631 apply (metis NPrf.intros(5)) |
|
632 apply(simp) |
|
633 apply(erule NPrf.cases) |
|
634 apply(simp_all)[7] |
|
635 apply(simp) |
|
636 apply(erule NPrf.cases) |
|
637 apply(simp_all)[7] |
|
638 apply (metis NPrf.intros(2)) |
|
639 apply (metis NPrf.intros(3)) |
|
640 apply(simp) |
|
641 apply(case_tac "nullable r1") |
|
642 apply(simp) |
|
643 apply(erule NPrf.cases) |
|
644 apply(simp_all)[7] |
|
645 apply(auto)[1] |
|
646 apply(erule NPrf.cases) |
|
647 apply(simp_all)[7] |
|
648 apply(auto)[1] |
|
649 apply (metis NPrf.intros(1)) |
|
650 apply(auto)[1] |
|
651 oops |
|
652 |
|
653 lemma v3_proj: |
713 lemma v3_proj: |
654 assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s" |
714 assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s" |
655 shows "\<Turnstile> (projval r c v) : der c r" |
715 shows "\<Turnstile> (projval r c v) : der c r" |
656 using assms |
716 using assms |
657 apply(induct rule: NPrf.induct) |
717 apply(induct rule: NPrf.induct) |
767 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
826 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
768 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
827 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
769 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
828 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
770 \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
829 \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
771 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
830 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
772 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Star vs; flat v \<noteq> []\<rbrakk> \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Star (v # vs)" |
831 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Star vs; flat v \<noteq> []\<rbrakk> |
|
832 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Star (v # vs)" |
773 | "[] \<in> STAR r \<rightarrow> Star []" |
833 | "[] \<in> STAR r \<rightarrow> Star []" |
774 |
834 |
775 lemma PMatch_mkeps: |
835 lemma PMatch_mkeps: |
776 assumes "nullable r" |
836 assumes "nullable r" |
777 shows "[] \<in> r \<rightarrow> mkeps r" |
837 shows "[] \<in> r \<rightarrow> mkeps r" |
817 apply (metis NPrf.intros(4)) |
877 apply (metis NPrf.intros(4)) |
818 apply (metis NPrf.intros(5)) |
878 apply (metis NPrf.intros(5)) |
819 apply (metis NPrf.intros(2)) |
879 apply (metis NPrf.intros(2)) |
820 apply (metis NPrf.intros(3)) |
880 apply (metis NPrf.intros(3)) |
821 apply (metis NPrf.intros(1)) |
881 apply (metis NPrf.intros(1)) |
822 apply (metis NPrf.intros(7) PMatch1(2)) |
882 apply(rule NPrf.intros) |
|
883 apply(simp) |
|
884 apply(simp) |
|
885 apply(simp) |
823 apply(rule NPrf.intros) |
886 apply(rule NPrf.intros) |
824 done |
887 done |
825 |
888 |
826 lemma PMatch_Values: |
889 lemma PMatch_Values: |
827 assumes "s \<in> r \<rightarrow> v" |
890 assumes "s \<in> r \<rightarrow> v" |
852 apply(simp_all)[7] |
915 apply(simp_all)[7] |
853 apply (metis PMatch.intros(3)) |
916 apply (metis PMatch.intros(3)) |
854 apply(clarify) |
917 apply(clarify) |
855 apply(rule PMatch.intros) |
918 apply(rule PMatch.intros) |
856 apply metis |
919 apply metis |
857 apply(simp add: L_flat_Prf) |
920 apply(simp add: L_flat_NPrf) |
858 apply(auto)[1] |
921 apply(auto)[1] |
859 apply(subgoal_tac "\<Turnstile> v : r1") |
|
860 apply(frule_tac c="c" in v3_proj) |
922 apply(frule_tac c="c" in v3_proj) |
861 apply metis |
923 apply metis |
862 apply(drule_tac x="projval r1 c v" in spec) |
924 apply(drule_tac x="projval r1 c v" in spec) |
863 apply(drule mp) |
925 apply(drule mp) |
864 apply (metis v4_proj2) |
926 apply (metis v4_proj2) |
865 apply (metis NPrf_imp_Prf) |
927 apply (metis NPrf_imp_Prf) |
866 defer |
|
867 (* SEQ case *) |
928 (* SEQ case *) |
868 apply(case_tac "nullable r1") |
929 apply(case_tac "nullable r1") |
869 apply(simp) |
930 apply(simp) |
870 prefer 2 |
931 prefer 2 |
871 apply(simp) |
932 apply(simp) |
875 apply(subst append.simps(2)[symmetric]) |
936 apply(subst append.simps(2)[symmetric]) |
876 apply(rule PMatch.intros) |
937 apply(rule PMatch.intros) |
877 apply metis |
938 apply metis |
878 apply metis |
939 apply metis |
879 apply(auto)[1] |
940 apply(auto)[1] |
880 apply(simp add: L_flat_Prf) |
941 apply(simp add: L_flat_NPrf) |
881 apply(auto)[1] |
942 apply(auto)[1] |
882 apply(subgoal_tac "\<Turnstile> v : r1") |
|
883 apply(frule_tac c="c" in v3_proj) |
943 apply(frule_tac c="c" in v3_proj) |
884 apply metis |
944 apply metis |
885 apply(drule_tac x="s3" in spec) |
945 apply(drule_tac x="s3" in spec) |
886 apply(drule mp) |
946 apply(drule mp) |
887 apply(rule_tac x="projval r1 c v" in exI) |
947 apply(rule_tac x="projval r1 c v" in exI) |
888 apply(rule conjI) |
948 apply(rule conjI) |
889 apply (metis v4_proj2) |
949 apply (metis v4_proj2) |
890 apply (metis NPrf_imp_Prf) |
950 apply (metis NPrf_imp_Prf) |
891 apply metis |
951 apply metis |
892 defer |
|
893 (* nullable case *) |
952 (* nullable case *) |
894 apply(erule PMatch.cases) |
953 apply(erule PMatch.cases) |
895 apply(simp_all)[7] |
954 apply(simp_all)[7] |
896 apply(clarify) |
955 apply(clarify) |
897 apply(erule PMatch.cases) |
956 apply(erule PMatch.cases) |
900 apply(subst append.simps(2)[symmetric]) |
959 apply(subst append.simps(2)[symmetric]) |
901 apply(rule PMatch.intros) |
960 apply(rule PMatch.intros) |
902 apply metis |
961 apply metis |
903 apply metis |
962 apply metis |
904 apply(auto)[1] |
963 apply(auto)[1] |
905 apply(simp add: L_flat_Prf) |
964 apply(simp add: L_flat_NPrf) |
906 apply(auto)[1] |
965 apply(auto)[1] |
907 apply(subgoal_tac "\<Turnstile> v : r1") |
|
908 apply(frule_tac c="c" in v3_proj) |
966 apply(frule_tac c="c" in v3_proj) |
909 apply metis |
967 apply metis |
910 apply(drule_tac x="s3" in spec) |
968 apply(drule_tac x="s3" in spec) |
911 apply(drule mp) |
969 apply(drule mp) |
912 apply (metis NPrf_imp_Prf v4_proj2) |
970 apply (metis NPrf_imp_Prf v4_proj2) |
913 apply(simp) |
971 apply(simp) |
914 defer |
|
915 (* interesting case *) |
972 (* interesting case *) |
916 apply(clarify) |
973 apply(clarify) |
917 apply(simp) |
974 apply(simp) |
918 apply(subst (asm) L.simps(4)[symmetric]) |
975 apply(subst (asm) L.simps(4)[symmetric]) |
919 apply(simp only: L_flat_Prf) |
976 apply(simp only: L_flat_Prf) |
921 apply(subst append.simps(1)[symmetric]) |
978 apply(subst append.simps(1)[symmetric]) |
922 apply(rule PMatch.intros) |
979 apply(rule PMatch.intros) |
923 apply (metis PMatch_mkeps) |
980 apply (metis PMatch_mkeps) |
924 apply metis |
981 apply metis |
925 apply(auto) |
982 apply(auto) |
926 apply(simp only: L_flat_Prf) |
983 apply(simp only: L_flat_NPrf) |
927 apply(simp) |
984 apply(simp) |
928 apply(auto) |
985 apply(auto) |
929 apply(drule_tac x="Seq (projval r1 c v) vb" in spec) |
986 apply(drule_tac x="Seq (projval r1 c v) vb" in spec) |
930 apply(drule mp) |
987 apply(drule mp) |
931 apply(simp) |
988 apply(simp) |
932 apply(subgoal_tac "\<Turnstile> v : r1") |
|
933 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2) |
989 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2) |
934 defer |
|
935 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1") |
990 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1") |
936 apply (metis Prf.intros(1)) |
991 apply (metis NPrf_imp_Prf Prf.intros(1)) |
937 apply(rule NPrf_imp_Prf) |
992 apply(rule NPrf_imp_Prf) |
938 apply(rule v3_proj) |
993 apply(rule v3_proj) |
939 defer |
994 apply(simp) |
940 apply (metis Cons_eq_append_conv) |
995 apply (metis Cons_eq_append_conv) |
941 (* Star case *) |
996 (* Star case *) |
942 apply(erule PMatch.cases) |
997 apply(erule PMatch.cases) |
943 apply(simp_all)[7] |
998 apply(simp_all)[7] |
944 apply(clarify) |
999 apply(clarify) |
947 apply(erule PMatch.cases) |
1002 apply(erule PMatch.cases) |
948 apply(simp_all)[7] |
1003 apply(simp_all)[7] |
949 apply(subst append.simps(2)[symmetric]) |
1004 apply(subst append.simps(2)[symmetric]) |
950 apply(rule PMatch.intros) |
1005 apply(rule PMatch.intros) |
951 apply metis |
1006 apply metis |
952 apply (metis Nil_is_append_conv PMatch.intros(6)) |
1007 apply(auto)[1] |
953 apply (metis PMatch1(2) list.distinct(1)) |
1008 apply(rule PMatch.intros) |
954 apply(auto)[1] |
1009 apply(simp) |
955 (* HERE *) |
1010 apply(simp) |
956 (* oops *) |
1011 apply(simp) |
|
1012 apply(subst v4) |
|
1013 apply (metis NPrf_imp_Prf PMatch1N) |
|
1014 apply(simp) |
|
1015 apply (metis PMatch.intros(6) PMatch.intros(7) PMatch1(2) append_Nil2 list.discI) |
|
1016 done |
957 |
1017 |
958 |
1018 |
959 |
1019 |
960 lemma lex_correct1: |
1020 lemma lex_correct1: |
961 assumes "s \<notin> L r" |
1021 assumes "s \<notin> L r" |
979 apply(induct s arbitrary: r) |
1039 apply(induct s arbitrary: r) |
980 apply(simp) |
1040 apply(simp) |
981 apply (metis mkeps_flat mkeps_nullable nullable_correctness) |
1041 apply (metis mkeps_flat mkeps_nullable nullable_correctness) |
982 apply(drule_tac x="der a r" in meta_spec) |
1042 apply(drule_tac x="der a r" in meta_spec) |
983 apply(drule meta_mp) |
1043 apply(drule meta_mp) |
984 apply(simp add: L_flat_Prf) |
1044 apply(simp add: L_flat_NPrf) |
985 apply(auto) |
1045 apply(auto) |
986 apply (metis v3_proj v4_proj2) |
1046 apply (metis v3_proj v4_proj2) |
987 apply (metis v3) |
1047 apply (metis v3) |
988 apply(rule v4) |
1048 apply(rule v4) |
989 by metis |
1049 by metis |
995 apply(induct s arbitrary: r) |
1055 apply(induct s arbitrary: r) |
996 apply(simp) |
1056 apply(simp) |
997 apply (metis PMatch_mkeps nullable_correctness) |
1057 apply (metis PMatch_mkeps nullable_correctness) |
998 apply(drule_tac x="der a r" in meta_spec) |
1058 apply(drule_tac x="der a r" in meta_spec) |
999 apply(drule meta_mp) |
1059 apply(drule meta_mp) |
1000 apply(simp add: L_flat_Prf) |
1060 apply(simp add: L_flat_NPrf) |
1001 apply(auto) |
1061 apply(auto) |
1002 apply (metis v3_proj v4_proj2) |
1062 apply (metis v3_proj v4_proj2) |
1003 apply(rule PMatch2) |
1063 apply(rule PMatch2) |
1004 apply(simp) |
1064 apply(simp) |
1005 done |
1065 done |
1013 apply (metis PMatch_mkeps nullable_correctness) |
1073 apply (metis PMatch_mkeps nullable_correctness) |
1014 apply(simp) |
1074 apply(simp) |
1015 apply(rule PMatch2) |
1075 apply(rule PMatch2) |
1016 apply(drule_tac x="der a r" in meta_spec) |
1076 apply(drule_tac x="der a r" in meta_spec) |
1017 apply(drule meta_mp) |
1077 apply(drule meta_mp) |
1018 apply(simp add: L_flat_Prf) |
1078 apply(simp add: L_flat_NPrf) |
1019 apply(auto) |
1079 apply(auto) |
1020 apply (metis v3_proj v4_proj2) |
1080 apply (metis v3_proj v4_proj2) |
1021 done |
1081 done |
1022 |
1082 |
1023 lemma |
1083 lemma |
1024 "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))" |
1084 "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))" |
1025 apply(simp) |
1085 apply(simp) |
1026 done |
1086 done |
1027 |
1087 |
|
1088 |
|
1089 (* NOT DONE YET *) |
1028 |
1090 |
1029 section {* Sulzmann's Ordering of values *} |
1091 section {* Sulzmann's Ordering of values *} |
1030 |
1092 |
1031 thm PMatch.intros |
1093 thm PMatch.intros |
1032 |
1094 |