808 section {* Lexer including simplifications *}

   809 

   810 

   811 fun F_RIGHT where

   812   "F_RIGHT f v = Right (f v)"

   813 

   814 fun F_LEFT where

   815   "F_LEFT f v = Left (f v)"

   816 

   817 fun F_ALT where

   818   "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"

   819 | "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)"  

   820 | "F_ALT f1 f2 v = v"

   821 

   822 

   823 fun F_SEQ1 where

   824   "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"

   825 

   826 fun F_SEQ2 where 

   827   "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"

   828 

   829 fun F_SEQ where 

   830   "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"

   831 | "F_SEQ f1 f2 v = v"

   832 

   833 fun simp_ALT where

   834   "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"

   835 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"

   836 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"

   837 

   838 fun simp_SEQ where

   839   "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"

   840 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"

   841 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  

   842  

   843 lemma simp_SEQ_simps:

   844   "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))

   845                     else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))

   846                     else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"

   847 apply(auto)

   848 apply(case_tac p1)

   849 apply(case_tac p2)

   850 apply(simp)

   851 apply(case_tac p1)

   852 apply(case_tac p2)

   853 apply(simp)

   854 apply(case_tac a)

   855 apply(simp_all)

   856 apply(case_tac p1)

   857 apply(case_tac p2)

   858 apply(simp)

   859 apply(case_tac p1)

   860 apply(case_tac p2)

   861 apply(simp)

   862 apply(case_tac a)

   863 apply(simp_all)

   864 apply(case_tac aa)

   865 apply(simp_all)

   866 apply(auto)

   867 apply(case_tac aa)

   868 apply(simp_all)

   869 apply(case_tac aa)

   870 apply(simp_all)

   871 apply(case_tac aa)

   872 apply(simp_all)

   873 apply(case_tac aa)

   874 apply(simp_all)

   875 done

   876 

   877 lemma simp_ALT_simps:

   878   "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))

   879                     else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))

   880                     else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"

   881 apply(auto)

   882 apply(case_tac p1)

   883 apply(case_tac p2)

   884 apply(simp)

   885 apply(case_tac p1)

   886 apply(case_tac p2)

   887 apply(simp)

   888 apply(case_tac a)

   889 apply(simp_all)

   890 apply(case_tac p1)

   891 apply(case_tac p2)

   892 apply(simp)

   893 apply(case_tac p1)

   894 apply(case_tac p2)

   895 apply(simp)

   896 apply(case_tac a)

   897 apply(simp_all)

   898 apply(case_tac aa)

   899 apply(simp_all)

   900 apply(auto)

   901 apply(case_tac aa)

   902 apply(simp_all)

   903 apply(case_tac aa)

   904 apply(simp_all)

   905 apply(case_tac aa)

   906 apply(simp_all)

   907 apply(case_tac aa)

   908 apply(simp_all)

   909 done

   910 

   911 

   912 fun 

   913   simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"

   914 where

   915   "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" 

   916 | "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" 

   917 | "simp r = (r, id)"

   918 

   919 fun 

   920   slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"

   921 where

   922   "slexer r [] = (if nullable r then Some(mkeps r) else None)"

   923 | "slexer r (c#s) = (let (rs, fr) = simp (der c r) in

   924                          (case (slexer rs s) of  

   925                             None \<Rightarrow> None

   926                           | Some(v) \<Rightarrow> Some(injval r c (fr v))))"

   927 

   928 

   929 lemma L_fst_simp:

   930   shows "L(r) = L(fst (simp r))"

   931 using assms

   932 apply(induct r rule: rexp.induct)

   933 apply(auto simp add: simp_SEQ_simps simp_ALT_simps)

   934 done

   935 

   936 lemma 

   937   shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))"

   938 using assms

   939 apply(induct r arbitrary: v rule: simp.induct)

   940 apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros)

   941 using Prf_elims(3) apply blast

   942 apply(erule Prf_elims)

   943 apply(simp)

   944 apply(clarify)

   945 apply(blast)

   946 apply(simp)

   947 apply(erule Prf_elims)

   948 apply(simp)

   949 apply(simp)

   950 apply(clarify)

   951 apply(blast)

   952 apply(erule Prf_elims)

   953 apply(case_tac v)

   954 apply(simp_all)

   955 apply(rule Prf.intros)

   956 apply(clarify)

   957 apply(simp)

   958 apply(case_tac v)

   959 apply(simp_all)

   960 apply(rule Prf.intros)

   961 apply(clarify)

   962 apply(simp)

   963 apply(erule Prf_elims)

   964 apply(simp)

   965 apply(rule Prf.intros)

   966 apply(simp)

   967 apply(simp)

   968 apply(rule Prf.intros)

   969 apply(simp)

   970 apply(erule Prf_elims)

   971 apply(simp)

   972 apply(blast)

   973 apply(rule Prf.intros)

   974 apply(erule Prf_elims)

   975 apply(simp)

   976 apply(rule Prf.intros)

   977 apply(erule Prf_elims)

   978 apply(simp)

   979 apply(rule Prf.intros)

   980 apply(erule Prf_elims)

   981 apply(simp)

   982 apply(clarify)

   983 apply(blast)

   984 apply(rule Prf.intros)

   985 apply(blast)

   986 using Prf.intros(4) apply blast

   987 apply(erule Prf_elims)

   988 apply(simp)

   989 apply(clarify)

   990 apply(blast)

   991 apply(rule Prf.intros)

   992 using Prf.intros(4) apply blast

   993 apply blast

   994 apply(erule Prf_elims)

   995 apply(case_tac v)

   996 apply(simp_all)

   997 apply(rule Prf.intros)

   998 apply(clarify)

   999 apply(simp)

  1000 apply(clarify)

  1001 apply(blast)

  1002 apply(erule Prf_elims)

  1003 apply(case_tac v)

  1004 apply(simp_all)

  1005 apply(rule Prf.intros)

  1006 apply(clarify)

  1007 apply(simp)

  1008 apply(simp)

  1009 done

  1010 

  1011 lemma Posix_simp_nullable:

  1012   assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v"

  1013   shows "((snd (simp r)) v) = mkeps r"

  1014 using assms 

  1015 apply(induct r arbitrary: v)

  1016 apply(auto simp add: simp_SEQ_simps simp_ALT_simps)

  1017 apply(erule Posix_elims)

  1018 apply(simp)

  1019 apply(erule Posix_elims)

  1020 apply(clarify)

  1021 using Posix.intros(1) apply blast

  1022 using Posix.intros(1) apply blast

  1023 using Posix.intros(1) apply blast

  1024 apply(erule Posix_elims)

  1025 apply(simp)

  1026 apply(erule Posix_elims)

  1027 apply (metis L_fst_simp nullable.simps(1) nullable_correctness)

  1028 apply(erule Posix_elims)

  1029 apply(clarify)

  1030 apply(simp)

  1031 apply(clarify)

  1032 apply(simp)

  1033 apply(simp only: L_fst_simp[symmetric])

  1034 apply (simp add: nullable_correctness)

  1035 apply(erule Posix_elims)

  1036 using L_fst_simp Posix1(1) nullable_correctness apply blast

  1037 apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable)

  1038 apply(erule Posix_elims)

  1039 apply(clarify)

  1040 apply(simp)

  1041 apply(simp only: L_fst_simp[symmetric])

  1042 apply (simp add: nullable_correctness)

  1043 apply(erule Posix_elims)

  1044 apply(clarify)

  1045 apply(simp)

  1046 using L_fst_simp Posix1(1) nullable_correctness apply blast

  1047 apply(simp)

  1048 apply(erule Posix_elims)

  1049 apply(clarify)

  1050 apply(simp)

  1051 using Posix1(2) apply auto[1]

  1052 apply(simp)

  1053 done

  1054 

  1055 lemma Posix_simp:

  1056   assumes "s \<in> (fst (simp r)) \<rightarrow> v" 

  1057   shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"

  1058 using assms

  1059 apply(induct r arbitrary: s v rule: rexp.induct) 

  1060 apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps)

  1061 prefer 3

  1062 apply(erule Posix_elims)

  1063 apply(clarify)

  1064 apply(simp)

  1065 apply(rule Posix.intros)

  1066 apply(blast)

  1067 apply(blast)

  1068 apply(auto)[1]

  1069 apply(simp add: L_fst_simp[symmetric])

  1070 apply(auto)[1]

  1071 prefer 3

  1072 apply(rule Posix.intros)

  1073 apply(blast)

  1074 apply (metis L.simps(1) L_fst_simp equals0D)

  1075 prefer 3

  1076 apply(rule Posix.intros)

  1077 apply(blast)

  1078 prefer 3

  1079 apply(erule Posix_elims)

  1080 apply(clarify)

  1081 apply(simp)

  1082 apply(rule Posix.intros)

  1083 apply(blast)

  1084 apply(simp)

  1085 apply(rule Posix.intros)

  1086 apply(blast)

  1087 apply(simp add: L_fst_simp[symmetric])

  1088 apply(subst append.simps[symmetric])

  1089 apply(rule Posix.intros)

  1090 prefer 2

  1091 apply(blast)

  1092 prefer 2

  1093 apply(auto)[1]

  1094 apply (metis L_fst_simp Posix_elims(2) lex_correct3a)

  1095 apply(subst Posix_simp_nullable)

  1096 using Posix.intros(1) Posix1(1) nullable_correctness apply blast

  1097 apply(simp)

  1098 apply(rule Posix.intros)

  1099 apply(rule Posix_mkeps)

  1100 using Posix.intros(1) Posix1(1) nullable_correctness apply blast

  1101 apply(subst append_Nil2[symmetric])

  1102 apply(rule Posix.intros)

  1103 apply(blast)

  1104 apply(subst Posix_simp_nullable)

  1105 using Posix.intros(1) Posix1(1) nullable_correctness apply blast

  1106 apply(simp)

  1107 apply(rule Posix.intros)

  1108 apply(rule Posix_mkeps)

  1109 using Posix.intros(1) Posix1(1) nullable_correctness apply blast

  1110 apply(auto)

  1111 done

  1112 

  1113 lemma slexer_correctness:

  1114   shows "slexer r s = lexer r s"

  1115 apply(induct s arbitrary: r)

  1116 apply(simp)

  1117 apply(simp)

  1118 apply(auto split: option.split prod.split)

  1119 apply (metis L_fst_simp fst_conv lex_correct1a)

  1120 using L_fst_simp lex_correct1a apply fastforce

  1121 by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv)

  1122 

  1123