24 |
24 |
25 lemma seq_null [simp]: |
25 lemma seq_null [simp]: |
26 shows "A ;; {} = {}" |
26 shows "A ;; {} = {}" |
27 and "{} ;; A = {}" |
27 and "{} ;; A = {}" |
28 by (simp_all add: Sequ_def) |
28 by (simp_all add: Sequ_def) |
|
29 |
|
30 definition |
|
31 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
32 where |
|
33 "Der c A \<equiv> {s. [c] @ s \<in> A}" |
|
34 |
|
35 lemma Der_null [simp]: |
|
36 shows "Der c {} = {}" |
|
37 unfolding Der_def |
|
38 by auto |
|
39 |
|
40 lemma Der_empty [simp]: |
|
41 shows "Der c {[]} = {}" |
|
42 unfolding Der_def |
|
43 by auto |
|
44 |
|
45 lemma Der_char [simp]: |
|
46 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
47 unfolding Der_def |
|
48 by auto |
|
49 |
|
50 lemma Der_union [simp]: |
|
51 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
52 unfolding Der_def |
|
53 by auto |
|
54 |
|
55 lemma Der_seq [simp]: |
|
56 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
57 unfolding Der_def Sequ_def |
|
58 apply (auto simp add: Cons_eq_append_conv) |
|
59 done |
29 |
60 |
30 lemma seq_image: |
61 lemma seq_image: |
31 assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)" |
62 assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)" |
32 shows "f ` (A ;; B) = (f ` A) ;; (f ` B)" |
63 shows "f ` (A ;; B) = (f ` A) ;; (f ` B)" |
33 apply(auto simp add: Sequ_def image_def) |
64 apply(auto simp add: Sequ_def image_def) |
46 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
77 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
47 for A :: "string set" |
78 for A :: "string set" |
48 where |
79 where |
49 start[intro]: "[] \<in> A\<star>" |
80 start[intro]: "[] \<in> A\<star>" |
50 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
81 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
|
82 |
|
83 lemma star_cases: |
|
84 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
|
85 unfolding Sequ_def |
|
86 by (auto) (metis Star.simps) |
|
87 |
51 |
88 |
52 fun |
89 fun |
53 pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100) |
90 pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100) |
54 where |
91 where |
55 "A \<up> 0 = {[]}" |
92 "A \<up> 0 = {[]}" |
112 assumes a: "c # x \<in> A\<star>" |
149 assumes a: "c # x \<in> A\<star>" |
113 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
150 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
114 using a |
151 using a |
115 by (induct x\<equiv>"c # x" rule: Star.induct) |
152 by (induct x\<equiv>"c # x" rule: Star.induct) |
116 (auto simp add: append_eq_Cons_conv) |
153 (auto simp add: append_eq_Cons_conv) |
|
154 |
|
155 lemma Der_star [simp]: |
|
156 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
157 proof - |
|
158 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
159 |
|
160 by (simp only: star_cases[symmetric]) |
|
161 also have "... = Der c (A ;; A\<star>)" |
|
162 by (simp only: Der_union Der_empty) (simp) |
|
163 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
|
164 by simp |
|
165 also have "... = (Der c A) ;; A\<star>" |
|
166 unfolding Sequ_def Der_def |
|
167 by (auto dest: star_decomp) |
|
168 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
169 qed |
|
170 |
117 |
171 |
118 |
172 |
119 section {* Regular Expressions *} |
173 section {* Regular Expressions *} |
120 |
174 |
121 datatype rexp = |
175 datatype rexp = |
976 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
1038 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
977 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
1039 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
978 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
1040 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
979 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
1041 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
980 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
1042 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
981 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []\<rbrakk> |
1043 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
1044 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
982 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
1045 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
983 | "[] \<in> STAR r \<rightarrow> Stars []" |
1046 | "[] \<in> STAR r \<rightarrow> Stars []" |
984 |
1047 |
985 lemma PMatch_mkeps: |
1048 lemma PMatch_mkeps: |
986 assumes "nullable r" |
1049 assumes "nullable r" |
1033 apply(simp) |
1096 apply(simp) |
1034 apply(simp) |
1097 apply(simp) |
1035 apply(simp) |
1098 apply(simp) |
1036 apply(rule NPrf.intros) |
1099 apply(rule NPrf.intros) |
1037 done |
1100 done |
|
1101 |
|
1102 lemma PMatch_determ: |
|
1103 shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2" |
|
1104 and "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2" |
|
1105 apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts) |
|
1106 apply(erule PMatch.cases) |
|
1107 apply(simp_all)[7] |
|
1108 apply(erule PMatch.cases) |
|
1109 apply(simp_all)[7] |
|
1110 apply(erule PMatch.cases) |
|
1111 apply(simp_all)[7] |
|
1112 apply(erule PMatch.cases) |
|
1113 apply(simp_all)[7] |
|
1114 apply(erule PMatch.cases) |
|
1115 apply(simp_all)[7] |
|
1116 apply(erule PMatch.cases) |
|
1117 apply(simp_all)[7] |
|
1118 apply(clarify) |
|
1119 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a") |
|
1120 apply metis |
|
1121 apply(rule conjI) |
|
1122 apply(simp add: append_eq_append_conv2) |
|
1123 apply(auto)[1] |
|
1124 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1125 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1126 apply(simp add: append_eq_append_conv2) |
|
1127 apply(auto)[1] |
|
1128 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1129 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1130 apply(erule PMatch.cases) |
|
1131 apply(simp_all)[7] |
|
1132 apply(clarify) |
|
1133 apply(erule PMatch.cases) |
|
1134 apply(simp_all)[7] |
|
1135 apply(clarify) |
|
1136 apply (metis NPrf_flat_L PMatch1(2) PMatch1N) |
|
1137 apply(erule PMatch.cases) |
|
1138 apply(simp_all)[7] |
|
1139 apply(clarify) |
|
1140 apply(erule PMatch.cases) |
|
1141 apply(simp_all)[7] |
|
1142 apply(clarify) |
|
1143 apply (metis NPrf_flat_L PMatch1(2) PMatch1N) |
|
1144 (* star case *) |
|
1145 defer |
|
1146 apply(erule PMatch.cases) |
|
1147 apply(simp_all)[7] |
|
1148 apply(clarify) |
|
1149 apply(erule PMatch.cases) |
|
1150 apply(simp_all)[7] |
|
1151 apply(clarify) |
|
1152 apply (metis PMatch1(2)) |
|
1153 apply(rotate_tac 3) |
|
1154 apply(erule PMatch.cases) |
|
1155 apply(simp_all)[7] |
|
1156 apply(clarify) |
|
1157 apply(erule PMatch.cases) |
|
1158 apply(simp_all)[7] |
|
1159 apply(clarify) |
|
1160 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a") |
|
1161 apply metis |
|
1162 apply(simp add: append_eq_append_conv2) |
|
1163 apply(auto)[1] |
|
1164 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1165 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1166 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1167 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
1168 apply(erule PMatch.cases) |
|
1169 apply(simp_all)[7] |
|
1170 apply(clarify) |
|
1171 apply (metis PMatch1(2)) |
|
1172 apply(erule PMatch.cases) |
|
1173 apply(simp_all)[7] |
|
1174 apply(clarify) |
|
1175 apply(erule PMatch.cases) |
|
1176 apply(simp_all)[7] |
|
1177 apply(clarify) |
|
1178 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a") |
|
1179 apply(drule_tac x="s1 @ s2" in meta_spec) |
|
1180 apply(drule_tac x="rb" in meta_spec) |
|
1181 apply(drule_tac x="(va#vsa)" in meta_spec) |
|
1182 apply(simp) |
|
1183 apply(drule meta_mp) |
|
1184 apply (metis L.simps(6) PMatch.intros(6)) |
|
1185 apply (metis L.simps(6) PMatch.intros(6)) |
|
1186 apply(simp add: append_eq_append_conv2) |
|
1187 apply(auto)[1] |
|
1188 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N) |
|
1189 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N) |
|
1190 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N) |
|
1191 apply (metis L.simps(6) NPrf_flat_L PMatch1(2) PMatch1N) |
|
1192 apply (metis PMatch1(2)) |
|
1193 apply(erule PMatch.cases) |
|
1194 apply(simp_all)[7] |
|
1195 apply(clarify) |
|
1196 by (metis PMatch1(2)) |
|
1197 |
1038 |
1198 |
1039 lemma PMatch_Values: |
1199 lemma PMatch_Values: |
1040 assumes "s \<in> r \<rightarrow> v" |
1200 assumes "s \<in> r \<rightarrow> v" |
1041 shows "v \<in> Values r s" |
1201 shows "v \<in> Values r s" |
1042 using assms |
1202 using assms |
1157 apply(auto)[1] |
1317 apply(auto)[1] |
1158 apply(rule PMatch.intros) |
1318 apply(rule PMatch.intros) |
1159 apply(simp) |
1319 apply(simp) |
1160 apply(simp) |
1320 apply(simp) |
1161 apply(simp) |
1321 apply(simp) |
|
1322 apply (metis L.simps(6)) |
1162 apply(subst v4) |
1323 apply(subst v4) |
1163 apply (metis NPrf_imp_Prf PMatch1N) |
1324 apply (metis NPrf_imp_Prf PMatch1N) |
1164 apply(simp) |
1325 apply(simp) |
1165 apply (metis PMatch.intros(6) PMatch.intros(7) PMatch1(2) append_Nil2 list.discI) |
1326 apply(auto)[1] |
1166 done |
1327 apply(drule_tac x="s\<^sub>3" in spec) |
1167 |
1328 apply(drule mp) |
1168 |
1329 defer |
|
1330 apply metis |
|
1331 apply(clarify) |
|
1332 apply(drule_tac x="s1" in meta_spec) |
|
1333 apply(drule_tac x="v1" in meta_spec) |
|
1334 apply(simp) |
|
1335 apply(rotate_tac 2) |
|
1336 apply(drule PMatch.intros(6)) |
|
1337 apply(rule PMatch.intros(7)) |
|
1338 apply (metis PMatch1(1) list.distinct(1) v4) |
|
1339 apply (metis Nil_is_append_conv) |
|
1340 apply(simp) |
|
1341 apply(subst der_correctness) |
|
1342 apply(simp add: Der_def) |
|
1343 done |
1169 |
1344 |
1170 lemma lex_correct1: |
1345 lemma lex_correct1: |
1171 assumes "s \<notin> L r" |
1346 assumes "s \<notin> L r" |
1172 shows "lex r s = None" |
1347 shows "lex r s = None" |
1173 using assms |
1348 using assms |
1416 apply (metis Prf.intros(7) ValOrd.intros(11) ValOrd_refl not_Cons_self2) |
1591 apply (metis Prf.intros(7) ValOrd.intros(11) ValOrd_refl not_Cons_self2) |
1417 apply(erule ValOrd.cases) |
1592 apply(erule ValOrd.cases) |
1418 apply(simp_all) |
1593 apply(simp_all) |
1419 apply(erule ValOrd.cases) |
1594 apply(erule ValOrd.cases) |
1420 apply(simp_all) |
1595 apply(simp_all) |
1421 apply(erule ValOrd.cases) |
1596 apply(rotate_tac 3) |
1422 apply(simp_all) |
1597 apply(erule Prf.cases) |
1423 apply(erule ValOrd.cases) |
1598 apply(simp_all)[7] |
1424 apply(simp_all) |
1599 apply(clarify) |
1425 apply(erule ValOrd.cases) |
1600 apply(erule ValOrd.cases) |
1426 apply(simp_all) |
1601 apply(simp_all) |
1427 |
1602 apply(erule ValOrd.cases) |
1428 |
1603 apply(simp_all) |
|
1604 apply(clarify) |
|
1605 apply(rotate_tac 4) |
|
1606 apply(erule Prf.cases) |
|
1607 apply(simp_all)[7] |
|
1608 apply(clarify) |
|
1609 apply(erule ValOrd.cases) |
|
1610 apply(simp_all) |
|
1611 apply(erule ValOrd.cases) |
|
1612 apply(simp_all) |
|
1613 apply(clarify) |
|
1614 |
|
1615 |
|
1616 apply(erule ValOrd.cases) |
|
1617 apply(simp_all) |
|
1618 apply(auto)[1] |
|
1619 prefer 2 |
|
1620 prefer 3 |
|
1621 apply(auto)[1] |
|
1622 apply(erule Prf.cases) |
|
1623 apply(simp_all)[7] |
|
1624 apply(erule Prf.cases) |
|
1625 apply(simp_all)[7] |
|
1626 apply(clarify) |
|
1627 apply(rotate_tac 3) |
|
1628 apply(erule ValOrd.cases) |
|
1629 apply(simp_all) |
|
1630 apply(auto)[1] |
1429 oops |
1631 oops |
1430 |
1632 |
1431 |
1633 |
1432 (* |
1634 (* |
1433 |
1635 |