461 done

   462 

   463 lemma PMatch1a:

   464   assumes "s \<in> r \<rightarrow> v"

   465   shows "s \<in> L r"

   466 using assms

   467 apply(induct s r v rule: PMatch.induct)

   468 apply(auto simp add: Sequ_def)

   794 section {* Attic stuff below *}

   795 

   796 section {* Projection function *}

   797 

   798 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"

   799 where

   800   "projval (CHAR d) c _ = Void"

   801 | "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"

   802 | "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"

   803 | "projval (SEQ r1 r2) c (Seq v1 v2) = 

   804      (if flat v1 = [] then Right(projval r2 c v2) 

   805       else if nullable r1 then Left (Seq (projval r1 c v1) v2)

   806                           else Seq (projval r1 c v1) v2)"

   807 | "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"

   808 

   809 

   810 

   811 section {* Values Sets *}

   812 

   813 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)

   814 where

   815   "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"

   816 

   817 definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)

   818 where

   819   "s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"

   820 

   821 lemma length_sprefix:

   822   "s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"

   823 unfolding sprefix_def prefix_def

   824 by (auto)

   825 

   826 definition Prefixes :: "string \<Rightarrow> string set" where

   827   "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"

   828 

   829 definition Suffixes :: "string \<Rightarrow> string set" where

   830   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"

   831 

   832 definition SPrefixes :: "string \<Rightarrow> string set" where

   833   "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"

   834 

   835 definition SSuffixes :: "string \<Rightarrow> string set" where

   836   "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"

   837 

   838 lemma Suffixes_in: 

   839   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"

   840 unfolding Suffixes_def Prefixes_def prefix_def image_def

   841 apply(auto)

   842 by (metis rev_rev_ident)

   843 

   844 lemma SSuffixes_in: 

   845   "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"

   846 unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def

   847 apply(auto)

   848 by (metis append_self_conv rev.simps(1) rev_rev_ident)

   849 

   850 lemma Prefixes_Cons:

   851   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"

   852 unfolding Prefixes_def prefix_def

   853 apply(auto simp add: append_eq_Cons_conv) 

   854 done

   855 

   856 lemma finite_Prefixes:

   857   "finite (Prefixes s)"

   858 apply(induct s)

   859 apply(auto simp add: Prefixes_def prefix_def)[1]

   860 apply(simp add: Prefixes_Cons)

   861 done

   862 

   863 lemma finite_Suffixes:

   864   "finite (Suffixes s)"

   865 unfolding Suffixes_def

   866 apply(rule finite_imageI)

   867 apply(rule finite_Prefixes)

   868 done

   869 

   870 lemma prefix_Cons:

   871   "((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"

   872 apply(auto simp add: prefix_def)

   873 done

   874 

   875 lemma prefix_append:

   876   "((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"

   877 apply(induct s)

   878 apply(simp)

   879 apply(simp add: prefix_Cons)

   880 done

   881 

   882 

   883 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where

   884   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"

   885 

   886 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where

   887   "rest v s \<equiv> drop (length (flat v)) s"

   888 

   889 lemma rest_Nil:

   890   "rest v [] = []"

   891 apply(simp add: rest_def)

   892 done

   893 

   894 lemma rest_Suffixes:

   895   "rest v s \<in> Suffixes s"

   896 unfolding rest_def

   897 by (metis Suffixes_in append_take_drop_id)

   898 

   899 lemma Values_recs:

   900   "Values (ZERO) s = {}"

   901   "Values (ONE) s = {Void}"

   902   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 

   903   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"

   904   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"

   905   "Values (STAR r) s = 

   906       {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"

   907 unfolding Values_def

   908 apply(auto)

   909 (*ZERO*)

   910 apply(erule Prf.cases)

   911 apply(simp_all)[7]

   912 (*ONE*)

   913 apply(erule Prf.cases)

   914 apply(simp_all)[7]

   915 apply(rule Prf.intros)

   916 apply (metis append_Nil prefix_def)

   917 (*CHAR*)

   918 apply(erule Prf.cases)

   919 apply(simp_all)[7]

   920 apply(rule Prf.intros)

   921 apply(erule Prf.cases)

   922 apply(simp_all)[7]

   923 (*ALT*)

   924 apply(erule Prf.cases)

   925 apply(simp_all)[7]

   926 apply (metis Prf.intros(2))

   927 apply (metis Prf.intros(3))

   928 (*SEQ*)

   929 apply(erule Prf.cases)

   930 apply(simp_all)[7]

   931 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   932 apply (metis Prf.intros(1))

   933 apply (simp add: append_eq_conv_conj prefix_def rest_def)

   934 (*STAR*)

   935 apply(erule Prf.cases)

   936 apply(simp_all)[7]

   937 apply(rule conjI)

   938 apply(simp add: prefix_def)

   939 apply(auto)[1]

   940 apply(simp add: prefix_def)

   941 apply(auto)[1]

   942 apply (metis append_eq_conv_conj rest_def)

   943 apply (metis Prf.intros(6))

   944 apply (metis append_Nil prefix_def)

   945 apply (metis Prf.intros(7))

   946 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)

   947 

   948 lemma PMatch_Values:

   949   assumes "s \<in> r \<rightarrow> v"

   950   shows "v \<in> Values r s"

   951 using assms

   952 apply(simp add: Values_def PMatch1)

   953 by (metis append_Nil2 prefix_def)

   954 

   955 lemma finite_image_set2:

   956   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"

   957   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto

   958 

   959 

   960 section {* Connection with Sulzmann's Ordering of values *}

   961 

   962 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)

   963 where

   964   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 

   965 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 

   966 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"

   967 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"

   968 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"

   969 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"

   970 | "Void \<succ>ONE Void"

   971 | "(Char c) \<succ>(CHAR c) (Char c)"

   972 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"

   973 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"

   974 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"

   975 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"

   976 | "(Stars []) \<succ>(STAR r) (Stars [])"

   977 

   978 

   979 (* non-problematic values...needed in order to fix the *) 

   980 (* proj lemma in Sulzmann & lu *)

   981 

   982 inductive 

   983   NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)

   984 where

   985  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"

   986 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"

   987 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"

   988 | "\<Turnstile> Void : ONE"

   989 | "\<Turnstile> Char c : CHAR c"

   990 | "\<Turnstile> Stars [] : STAR r"

   991 | "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"

   992 

   993 lemma NPrf_imp_Prf:

   994   assumes "\<Turnstile> v : r" 

   995   shows "\<turnstile> v : r"

   996 using assms

   997 apply(induct)

   998 apply(auto intro: Prf.intros)

   999 done

  1000 

  1001 lemma Star_valN:

  1002   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"

  1003   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r)"

  1004 using assms

  1005 apply(induct ss)

  1006 apply(auto)

  1007 apply (metis empty_iff list.set(1))

  1008 by (metis concat.simps(2) list.simps(9) set_ConsD)

  1009 

  1010 lemma NPrf_Prf_val:

  1011   shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"

  1012   and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"

  1013 using assms

  1014 apply(induct v and vs arbitrary: r and r rule: compat_val.induct compat_val_list.induct)

  1015 apply(auto)[1]

  1016 apply(erule Prf.cases)

  1017 apply(simp_all)[7]

  1018 apply(rule_tac x="Void" in exI)

  1019 apply(simp)

  1020 apply(rule NPrf.intros)

  1021 apply(erule Prf.cases)

  1022 apply(simp_all)[7]

  1023 apply(rule_tac x="Char c" in exI)

  1024 apply(simp)

  1025 apply(rule NPrf.intros)

  1026 apply(erule Prf.cases)

  1027 apply(simp_all)[7]

  1028 apply(auto)[1]

  1029 apply(drule_tac x="r1" in meta_spec)

  1030 apply(drule_tac x="r2" in meta_spec)

  1031 apply(simp)

  1032 apply(auto)[1]

  1033 apply(rule_tac x="Seq v' v'a" in exI)

  1034 apply(simp)

  1035 apply (metis NPrf.intros(1))

  1036 apply(erule Prf.cases)

  1037 apply(simp_all)[7]

  1038 apply(clarify)

  1039 apply(drule_tac x="r2" in meta_spec)

  1040 apply(simp)

  1041 apply(auto)[1]

  1042 apply(rule_tac x="Right v'" in exI)

  1043 apply(simp)

  1044 apply (metis NPrf.intros)

  1045 apply(erule Prf.cases)

  1046 apply(simp_all)[7]

  1047 apply(clarify)

  1048 apply(drule_tac x="r1" in meta_spec)

  1049 apply(simp)

  1050 apply(auto)[1]

  1051 apply(rule_tac x="Left v'" in exI)

  1052 apply(simp)

  1053 apply (metis NPrf.intros)

  1054 apply(drule_tac x="r" in meta_spec)

  1055 apply(simp)

  1056 apply(auto)[1]

  1057 apply(rule_tac x="Stars vs'" in exI)

  1058 apply(simp)

  1059 apply(rule_tac x="[]" in exI)

  1060 apply(simp)

  1061 apply(erule Prf.cases)

  1062 apply(simp_all)[7]

  1063 apply (metis NPrf.intros(6))

  1064 apply(erule Prf.cases)

  1065 apply(simp_all)[7]

  1066 apply(auto)[1]

  1067 apply(drule_tac x="ra" in meta_spec)

  1068 apply(simp)

  1069 apply(drule_tac x="STAR ra" in meta_spec)

  1070 apply(simp)

  1071 apply(auto)

  1072 apply(case_tac "flat v = []")

  1073 apply(rule_tac x="vs'" in exI)

  1074 apply(simp)

  1075 apply(rule_tac x="v' # vs'" in exI)

  1076 apply(simp)

  1077 apply(rule NPrf.intros)

  1078 apply(auto)

  1079 done

  1080 

  1081 lemma NPrf_Prf:

  1082   shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"

  1083 apply(auto)

  1084 apply (metis NPrf_Prf_val(1))

  1085 by (metis NPrf_imp_Prf)

  1086 

  1087 lemma NPrf_flat_L:

  1088   assumes "\<Turnstile> v : r" shows "flat v \<in> L r"

  1089 using assms

  1090 by (metis NPrf_imp_Prf Prf_flat_L)

  1091 

  1092 

  1093 lemma L_flat_NPrf:

  1094   "L(r) = {flat v | v. \<Turnstile> v : r}"

  1095 by (metis L_flat_Prf NPrf_Prf)

  1096 

  1097 

  1098 

  1099 lemma v3_proj:

  1100   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"

  1101   shows "\<Turnstile> (projval r c v) : der c r"

  1102 using assms

  1103 apply(induct rule: NPrf.induct)

  1104 prefer 4

  1105 apply(simp)

  1106 prefer 4

  1107 apply(simp)

  1108 apply (metis NPrf.intros(4))

  1109 prefer 2

  1110 apply(simp)

  1111 apply (metis NPrf.intros(2))

  1112 prefer 2

  1113 apply(simp)

  1114 apply (metis NPrf.intros(3))

  1115 apply(auto)

  1116 apply(rule NPrf.intros)

  1117 apply(simp)

  1118 apply (metis NPrf_imp_Prf not_nullable_flat)

  1119 apply(rule NPrf.intros)

  1120 apply(rule NPrf.intros)

  1121 apply (metis Cons_eq_append_conv)

  1122 apply(simp)

  1123 apply(rule NPrf.intros)

  1124 apply (metis Cons_eq_append_conv)

  1125 apply(simp)

  1126 (* Stars case *)

  1127 apply(rule NPrf.intros)

  1128 apply (metis Cons_eq_append_conv)

  1129 apply(auto)

  1130 done

  1131 

  1132 lemma v4_proj:

  1133   assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"

  1134   shows "c # flat (projval r c v) = flat v"

  1135 using assms

  1136 apply(induct rule: NPrf.induct)

  1137 prefer 4

  1138 apply(simp)

  1139 prefer 4

  1140 apply(simp)

  1141 prefer 2

  1142 apply(simp)

  1143 prefer 2

  1144 apply(simp)

  1145 apply(auto)

  1146 apply (metis Cons_eq_append_conv)

  1147 apply(simp add: append_eq_Cons_conv)

  1148 apply(auto)

  1149 done

  1150 

  1151 lemma v4_proj2:

  1152   assumes "\<Turnstile> v : r" and "(flat v) = c # s"

  1153   shows "flat (projval r c v) = s"

  1154 using assms

  1155 by (metis list.inject v4_proj)

  1156 

  1157 lemma PMatch1N:

  1158   assumes "s \<in> r \<rightarrow> v"

  1159   shows "\<Turnstile> v : r" 

  1160 using assms

  1161 apply(induct s r v rule: PMatch.induct)

  1162 apply(auto)

  1163 apply (metis NPrf.intros(4))

  1164 apply (metis NPrf.intros(5))

  1165 apply (metis NPrf.intros(2))

  1166 apply (metis NPrf.intros(3))

  1167 apply (metis NPrf.intros(1))

  1168 apply(rule NPrf.intros)

  1169 apply(simp)

  1170 apply(simp)

  1171 apply(simp)

  1172 apply(rule NPrf.intros)

  1173 done

  1174 

  1175 (* this version needs proj *)

  1176 lemma PMatch2:

  1177   assumes "s \<in> (der c r) \<rightarrow> v"

  1178   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"

  1179 using assms

  1180 apply(induct c r arbitrary: s v rule: der.induct)

  1181 apply(auto)

  1182 (* ZERO case *)

  1183 apply(erule PMatch.cases)

  1184 apply(simp_all)[7]

  1185 (* ONE case *)

  1186 apply(erule PMatch.cases)

  1187 apply(simp_all)[7]

  1188 (* CHAR case *)

  1189 apply(case_tac "c = d")

  1190 apply(simp)

  1191 apply(erule PMatch.cases)

  1192 apply(simp_all)[7]

  1193 apply (metis PMatch.intros(2))

  1194 apply(simp)

  1195 apply(erule PMatch.cases)

  1196 apply(simp_all)[7]

  1197 (* ALT case *)

  1198 apply(erule PMatch.cases)

  1199 apply(simp_all)[7]

  1200 apply (metis PMatch.intros(3))

  1201 apply(clarify)

  1202 apply(rule PMatch.intros)

  1203 apply metis

  1204 apply(simp add: der_correctness Der_def)

  1205 (* SEQ case *)

  1206 apply(case_tac "nullable r1")

  1207 apply(simp)

  1208 prefer 2

  1209 (* not-nullbale case *)

  1210 apply(simp)

  1211 apply(erule PMatch.cases)

  1212 apply(simp_all)[7]

  1213 apply(clarify)

  1214 apply(subst append.simps(2)[symmetric])

  1215 apply(rule PMatch.intros)

  1216 apply metis

  1217 apply metis

  1218 apply(auto)[1]

  1219 apply(simp add: der_correctness Der_def)

  1220 apply(auto)[1]

  1221 (* nullable case *)

  1222 apply(erule PMatch.cases)

  1223 apply(simp_all)[7]

  1224 (* left case *)

  1225 apply(clarify)

  1226 apply(erule PMatch.cases)

  1227 apply(simp_all)[4]

  1228 prefer 2

  1229 apply(clarify)

  1230 prefer 2

  1231 apply(clarify)

  1232 apply(clarify)

  1233 apply(simp (no_asm))

  1234 apply(subst append.simps(2)[symmetric])

  1235 apply(rule PMatch.intros)

  1236 apply metis

  1237 apply metis

  1238 apply(erule contrapos_nn)

  1239 apply(erule exE)+

  1240 apply(auto)[1]

  1241 apply(simp add: der_correctness Der_def)

  1242 apply metis

  1243 (* right interesting case *)

  1244 apply(clarify)

  1245 apply(simp)

  1246 apply(subst (asm) L.simps(4)[symmetric])

  1247 apply(simp only: L_flat_Prf)

  1248 apply(simp)

  1249 apply(subst append.simps(1)[symmetric])

  1250 apply(rule PMatch.intros)

  1251 apply (metis PMatch_mkeps)

  1252 apply metis

  1253 apply(auto)

  1254 apply(simp only: L_flat_NPrf)

  1255 apply(simp)

  1256 apply(auto)

  1257 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)

  1258 apply(drule mp)

  1259 apply(simp)

  1260 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)

  1261 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")

  1262 apply (metis NPrf_imp_Prf Prf.intros(1))

  1263 apply(rule NPrf_imp_Prf)

  1264 apply(rule v3_proj)

  1265 apply(simp)

  1266 apply (metis Cons_eq_append_conv)

  1267 (* Stars case *)

  1268 apply(erule PMatch.cases)

  1269 apply(simp_all)[7]

  1270 apply(clarify)

  1271 apply(rotate_tac 2)

  1272 apply(frule_tac PMatch1)

  1273 apply(erule PMatch.cases)

  1274 apply(simp_all)[7]

  1275 apply(subst append.simps(2)[symmetric])

  1276 apply(rule PMatch.intros)

  1277 apply metis

  1278 apply(auto)[1]

  1279 apply(rule PMatch.intros)

  1280 apply(simp)

  1281 apply(simp)

  1282 apply(simp)

  1283 apply (metis L.simps(6))

  1284 apply(subst Prf_injval_flat)

  1285 apply (metis NPrf_imp_Prf PMatch1N)

  1286 apply(simp)

  1287 apply(auto)[1]

  1288 apply(drule_tac x="s\<^sub>3" in spec)

  1289 apply(drule mp)

  1290 defer

  1291 apply metis

  1292 apply(clarify)

  1293 apply(drule_tac x="s1" in meta_spec)

  1294 apply(drule_tac x="v1" in meta_spec)

  1295 apply(simp)

  1296 apply(rotate_tac 2)

  1297 apply(drule PMatch.intros(6))

  1298 apply(rule PMatch.intros(7))

  1299 apply (metis PMatch1(1) list.distinct(1) Prf_injval_flat)

  1300 apply (metis Nil_is_append_conv)

  1301 apply(simp)

  1302 apply(subst der_correctness)

  1303 apply(simp add: Der_def)

  1304 done 

  1305 

  1306 lemma lex_correct4:

  1307   assumes "s \<in> L r"

  1308   shows "\<exists>v. matcher r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"

  1309 using lex_correct3[OF assms]

  1310 apply(auto)

  1311 apply (metis PMatch1N)

  1312 by (metis PMatch1(2))

  1313