398 lemma bder_retrieve: |
398 lemma bder_retrieve: |
399 assumes "\<Turnstile> v : der c (erase r)" |
399 assumes "\<Turnstile> v : der c (erase r)" |
400 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
400 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
401 using assms |
401 using assms |
402 apply(induct r arbitrary: v rule: erase.induct) |
402 apply(induct r arbitrary: v rule: erase.induct) |
403 apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) |
403 apply(simp) |
404 apply(case_tac va) |
404 apply(erule Prf_elims) |
405 apply(simp) |
405 apply(simp) |
406 apply(auto) |
406 apply(erule Prf_elims) |
407 by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq) |
407 apply(simp) |
408 |
408 apply(case_tac "c = ca") |
|
409 apply(simp) |
|
410 apply(erule Prf_elims) |
|
411 apply(simp) |
|
412 apply(simp) |
|
413 apply(erule Prf_elims) |
|
414 apply(simp) |
|
415 apply(erule Prf_elims) |
|
416 apply(simp) |
|
417 apply(simp) |
|
418 apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v) |
|
419 apply(erule Prf_elims) |
|
420 apply(simp) |
|
421 apply(simp) |
|
422 apply(case_tac rs) |
|
423 apply(simp) |
|
424 apply(simp) |
|
425 apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq) |
|
426 apply(simp) |
|
427 apply(case_tac "nullable (erase r1)") |
|
428 apply(simp) |
|
429 apply(erule Prf_elims) |
|
430 apply(subgoal_tac "bnullable r1") |
|
431 prefer 2 |
|
432 using bnullable_correctness apply blast |
|
433 apply(simp) |
|
434 apply(erule Prf_elims) |
|
435 apply(simp) |
|
436 apply(subgoal_tac "bnullable r1") |
|
437 prefer 2 |
|
438 using bnullable_correctness apply blast |
|
439 apply(simp) |
|
440 apply(simp add: retrieve_fuse2) |
|
441 apply(simp add: bmkeps_retrieve) |
|
442 apply(simp) |
|
443 apply(erule Prf_elims) |
|
444 apply(simp) |
|
445 using bnullable_correctness apply blast |
|
446 apply(rename_tac bs r v) |
|
447 apply(simp) |
|
448 apply(erule Prf_elims) |
|
449 apply(clarify) |
|
450 apply(erule Prf_elims) |
|
451 apply(clarify) |
|
452 apply(subst injval.simps) |
|
453 apply(simp del: retrieve.simps) |
|
454 apply(subst retrieve.simps) |
|
455 apply(subst retrieve.simps) |
|
456 apply(simp) |
|
457 apply(simp add: retrieve_fuse2) |
|
458 done |
|
459 |
|
460 |
409 |
461 |
410 lemma MAIN_decode: |
462 lemma MAIN_decode: |
411 assumes "\<Turnstile> v : ders s r" |
463 assumes "\<Turnstile> v : ders s r" |
412 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
464 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
413 using assms |
465 using assms |
423 case (snoc c s v) |
475 case (snoc c s v) |
424 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
476 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
425 Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact |
477 Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact |
426 have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact |
478 have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact |
427 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
479 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
428 by(simp add: Prf_injval ders_append) |
480 by (simp add: Prf_injval ders_append) |
429 have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" |
481 have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" |
430 by (simp add: flex_append) |
482 by (simp add: flex_append) |
431 also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" |
483 also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" |
432 using asm2 IH by simp |
484 using asm2 IH by simp |
433 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
485 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
434 using asm by(simp_all add: bder_retrieve ders_append) |
486 using asm by (simp_all add: bder_retrieve ders_append) |
435 finally show "Some (flex r id (s @ [c]) v) = |
487 finally show "Some (flex r id (s @ [c]) v) = |
436 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
488 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
437 qed |
489 qed |
|
490 |
|
491 |
|
492 definition blex where |
|
493 "blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None" |
|
494 |
438 |
495 |
439 |
496 |
440 definition blexer where |
497 definition blexer where |
441 "blexer r s \<equiv> if bnullable (bders (intern r) s) then |
498 "blexer r s \<equiv> if bnullable (bders (intern r) s) then |
442 decode (bmkeps (bders (intern r) s)) r else None" |
499 decode (bmkeps (bders (intern r) s)) r else None" |
962 apply(auto) |
1022 apply(auto) |
963 apply(rule nn1bb) |
1023 apply(rule nn1bb) |
964 apply(auto) |
1024 apply(auto) |
965 by (metis (mono_tags, hide_lams) imageE nn1c set_map) |
1025 by (metis (mono_tags, hide_lams) imageE nn1c set_map) |
966 |
1026 |
|
1027 lemma nn1d: |
|
1028 assumes "bsimp r = AALTs bs rs" |
|
1029 shows "\<forall>r1 \<in> set rs. \<forall> bs. r1 \<noteq> AALTs bs rs2" |
|
1030 using nn1b assms |
|
1031 by (metis nn1qq) |
|
1032 |
|
1033 lemma nn_flts: |
|
1034 assumes "nonnested (AALTs bs rs)" |
|
1035 shows "\<forall>r \<in> set (flts rs). nonalt r" |
|
1036 using assms |
|
1037 apply(induct rs arbitrary: bs rule: flts.induct) |
|
1038 apply(auto) |
|
1039 done |
|
1040 |
967 lemma rt: |
1041 lemma rt: |
968 shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)" |
1042 shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)" |
969 apply(induct rs) |
1043 apply(induct rs) |
970 apply(simp) |
1044 apply(simp) |
971 apply(simp) |
1045 apply(simp) |
972 apply(subst k0) |
1046 apply(subst k0) |
973 apply(simp) |
1047 apply(simp) |
974 by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1) |
1048 by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1) |
975 |
1049 |
|
1050 lemma bsimp_AALTs_qq: |
|
1051 assumes "1 < length rs" |
|
1052 shows "bsimp_AALTs bs rs = AALTs bs rs" |
|
1053 using assms |
|
1054 apply(case_tac rs) |
|
1055 apply(simp) |
|
1056 apply(case_tac list) |
|
1057 apply(simp_all) |
|
1058 done |
|
1059 |
976 lemma flts_idem: |
1060 lemma flts_idem: |
977 assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" |
1061 assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r" |
978 shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)" |
1062 shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)" |
979 using assms |
1063 using assms |
980 apply(induct rs) |
1064 apply(induct rs) |
1089 apply(case_tac x43) |
1173 apply(case_tac x43) |
1090 apply(simp_all) |
1174 apply(simp_all) |
1091 prefer 3 |
1175 prefer 3 |
1092 oops |
1176 oops |
1093 |
1177 |
|
1178 lemma ww: |
|
1179 shows "bsimp_AALTs bs [r] = fuse bs r" |
|
1180 by simp |
|
1181 |
|
1182 lemma flts_0: |
|
1183 assumes "nonnested (AALTs bs rs)" |
|
1184 shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO" |
|
1185 using assms |
|
1186 apply(induct rs arbitrary: bs rule: flts.induct) |
|
1187 apply(simp) |
|
1188 apply(simp) |
|
1189 defer |
|
1190 apply(simp) |
|
1191 apply(simp) |
|
1192 apply(simp) |
|
1193 apply(simp) |
|
1194 apply(rule ballI) |
|
1195 apply(simp) |
|
1196 done |
|
1197 |
|
1198 lemma q1: |
|
1199 shows "AZERO \<notin> set (flts (map bsimp rs))" |
|
1200 apply(induct rs) |
|
1201 apply(simp) |
|
1202 apply(simp) |
|
1203 apply(case_tac rs) |
|
1204 apply(simp) |
|
1205 |
|
1206 lemma cc: |
|
1207 assumes "bsimp (fuse bs' r) = (AALTs bs rs)" |
|
1208 shows "\<forall>r \<in> set rs. r \<noteq> AZERO" |
|
1209 using assms |
|
1210 apply(induct r arbitrary: rs bs bs' rule: bsimp.induct) |
|
1211 apply(simp) |
|
1212 apply(case_tac "bsimp r1 = AZERO") |
|
1213 apply simp |
|
1214 apply(case_tac "bsimp r2 = AZERO") |
|
1215 apply(simp) |
|
1216 apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'") |
|
1217 apply(auto)[1] |
|
1218 apply (simp add: bsimp_ASEQ0) |
|
1219 apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'") |
|
1220 apply(auto)[2] |
|
1221 apply (simp add: bsimp_ASEQ2) |
|
1222 using bsimp_fuse apply fastforce |
|
1223 apply (simp add: bsimp_ASEQ1) |
|
1224 prefer 2 |
|
1225 apply(simp) |
|
1226 defer |
|
1227 apply(simp) |
|
1228 apply(simp) |
|
1229 apply(simp) |
|
1230 (* AALT case *) |
|
1231 apply(simp only: fuse.simps) |
|
1232 apply(simp) |
|
1233 apply(case_tac "flts (map bsimp rs)") |
|
1234 apply(simp) |
|
1235 apply(simp) |
|
1236 apply(case_tac list) |
|
1237 apply(simp) |
|
1238 apply(case_tac a) |
|
1239 apply(simp_all) |
|
1240 apply(auto) |
|
1241 apply (metis ex_map_conv list.set_intros(1) nn1b nn1c nonalt.simps(1)) |
|
1242 apply(case_tac rs) |
|
1243 apply(simp) |
|
1244 apply(simp) |
|
1245 apply(case_tac list) |
|
1246 apply(simp) |
|
1247 |
|
1248 |
|
1249 apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO") |
|
1250 prefer 2 |
|
1251 apply(rule_tac bs="bs' @ bs1" in flts_0) |
|
1252 |
|
1253 |
|
1254 thm bsimp_AALTs_qq |
|
1255 apply(case_tac "1 < length rs") |
|
1256 apply(drule_tac bsimp_AALTs_qq) |
|
1257 apply(subgoal_tac "nonnested (AALTs bs rsa)") |
|
1258 prefer 2 |
|
1259 apply (metis nn1b) |
|
1260 apply(rule ballI) |
|
1261 apply(simp) |
|
1262 apply(drule_tac x="r" in meta_spec) |
|
1263 apply(simp) |
|
1264 (* HERE *) |
|
1265 apply(drule flts_0) |
|
1266 |
|
1267 |
|
1268 |
|
1269 apply(simp) |
|
1270 |
|
1271 |
|
1272 |
|
1273 |
|
1274 apply(subst |
|
1275 |
|
1276 apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims) |
|
1277 |
|
1278 prefer 2 |
|
1279 |
|
1280 |
|
1281 apply(induct r arbitrary: rs bs bs' rule: bsimp.induct) |
|
1282 apply(auto) |
|
1283 apply(case_tac "bsimp r1 = AZERO") |
|
1284 apply simp |
|
1285 apply(case_tac "bsimp r2 = AZERO") |
|
1286 apply(simp) |
|
1287 apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'") |
|
1288 apply(auto) |
|
1289 apply (simp add: bsimp_ASEQ0) |
|
1290 apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'") |
|
1291 apply(auto) |
|
1292 apply (simp add: bsimp_ASEQ2) |
|
1293 using bsimp_fuse apply fastforce |
|
1294 apply (simp add: bsimp_ASEQ1) |
|
1295 |
|
1296 |
|
1297 |
|
1298 apply(subst |
|
1299 |
|
1300 apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims) |
|
1301 |
|
1302 prefer 2 |
|
1303 |
|
1304 |
|
1305 |
|
1306 lemma ww1: |
|
1307 assumes "flts [r1] = [r2]" "r1 \<noteq> AZERO" |
|
1308 shows "r1 = r2" |
|
1309 using assms |
|
1310 apply(case_tac r1) |
|
1311 apply(simp) |
|
1312 apply(simp) |
|
1313 apply(simp) |
|
1314 apply(simp) |
|
1315 prefer 2 |
|
1316 apply(simp) |
|
1317 apply(simp) |
|
1318 apply(auto) |
|
1319 oops |
|
1320 |
1094 lemma bsimp_idem: |
1321 lemma bsimp_idem: |
1095 shows "bsimp (bsimp r) = bsimp r" |
1322 shows "bsimp (bsimp r) = bsimp r" |
1096 apply(induct r taking: "asize" rule: measure_induct) |
1323 apply(induct r taking: "asize" rule: measure_induct) |
1097 apply(case_tac x) |
1324 apply(case_tac x) |
1098 apply(simp) |
1325 apply(simp) |
1102 apply(simp) |
1329 apply(simp) |
1103 apply(simp) |
1330 apply(simp) |
1104 apply (simp add: bsimp_ASEQ_idem) |
1331 apply (simp add: bsimp_ASEQ_idem) |
1105 apply(clarify) |
1332 apply(clarify) |
1106 apply(case_tac x52) |
1333 apply(case_tac x52) |
1107 apply(simp) |
1334 apply(simp) |
1108 apply(simp) |
1335 (* AALT case where rs is of the form _ # _ *) |
|
1336 apply(clarify) |
|
1337 apply(simp) |
|
1338 apply(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1") |
|
1339 prefer 2 |
|
1340 apply(subst bsimp_AALTs_qq) |
|
1341 apply(auto)[1] |
|
1342 apply(simp) |
|
1343 prefer 2 |
|
1344 apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> |
|
1345 length (flts (bsimp a # map bsimp list)) = 1") |
|
1346 prefer 2 |
|
1347 apply(auto)[1] |
|
1348 using le_SucE apply blast |
|
1349 apply(erule disjE) |
|
1350 apply(simp) |
|
1351 apply(simp) |
|
1352 apply(subst k0) |
|
1353 apply(subst (2) k0) |
|
1354 apply(subst (asm) k0) |
|
1355 apply(simp) |
|
1356 apply(subgoal_tac "length (flts [bsimp a]) = 1 \<or> |
|
1357 length (flts (map bsimp list)) = 1") |
|
1358 prefer 2 |
|
1359 apply linarith |
|
1360 apply(erule disjE) |
|
1361 apply(simp) |
|
1362 prefer 2 |
|
1363 apply(simp) |
|
1364 apply(drule_tac x="AALTs x51 list" in spec) |
|
1365 apply(drule mp) |
|
1366 apply(simp) |
|
1367 using asize0 apply blast |
|
1368 apply(simp) |
|
1369 apply(frule_tac x="a" in spec) |
|
1370 apply(drule mp) |
|
1371 apply(simp) |
|
1372 apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]") |
|
1373 prefer 2 |
|
1374 apply (simp add: length_Suc_conv) |
|
1375 apply(clarify) |
|
1376 apply(simp only: ) |
|
1377 apply(case_tac "bsimp a = AZERO") |
|
1378 apply simp |
|
1379 apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs") |
|
1380 apply(clarify) |
|
1381 apply(simp) |
|
1382 apply(drule_tac x="AALTs bs rs" in spec) |
|
1383 apply(drule mp) |
|
1384 apply(simp) |
|
1385 apply (metis asize.simps(4) bsimp_size lessI less_le_trans trans_less_add1) |
|
1386 apply(simp) |
|
1387 |
|
1388 apply(subst ww) |
|
1389 apply(subst ww) |
|
1390 apply(frule_tac x="fuse x51 r" in spec) |
|
1391 apply(drule mp) |
|
1392 apply(simp) |
|
1393 apply (smt add.commute add_le_cancel_right fuse_size le_add2 le_trans list.map(1) list.simps(9) not_less not_less_eq rt sum_list.Cons) |
|
1394 apply(case_tac "bsimp a = AZERO") |
|
1395 apply simp |
|
1396 apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs") |
|
1397 apply(clarify) |
|
1398 |
|
1399 defer |
|
1400 |
|
1401 apply( |
|
1402 apply(case_tac a) |
|
1403 apply(simp_all) |
|
1404 apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]") |
|
1405 prefer 2 |
|
1406 apply (simp add: length_Suc_conv) |
|
1407 apply auto[1] |
|
1408 apply(case_tac |
|
1409 apply(clarify) |
|
1410 |
|
1411 defer |
|
1412 apply(auto)[1] |
|
1413 |
|
1414 |
1109 apply(subst k0) |
1415 apply(subst k0) |
1110 apply(subst (2) k0) |
1416 apply(subst (2) k0) |
1111 apply(case_tac "bsimp a = AZERO") |
1417 apply(case_tac "bsimp a = AZERO") |
1112 apply(simp) |
1418 apply(simp) |
1113 apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec) |
1419 apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec) |
1990 apply(subst blexer_simp_def) |
2296 apply(subst blexer_simp_def) |
1991 apply(subgoal_tac "\<not> bnullable (bders_simp (intern r) (a # s))") |
2297 apply(subgoal_tac "\<not> bnullable (bders_simp (intern r) (a # s))") |
1992 apply(simp) |
2298 apply(simp) |
1993 apply(subst bnullable_correctness[symmetric]) |
2299 apply(subst bnullable_correctness[symmetric]) |
1994 apply(simp) |
2300 apply(simp) |
|
2301 oops |
|
2302 |
|
2303 lemma flts_append: |
|
2304 "flts (xs1 @ xs2) = flts xs1 @ flts xs2" |
|
2305 apply(induct xs1 arbitrary: xs2 rule: rev_induct) |
|
2306 apply(auto) |
|
2307 apply(case_tac xs) |
|
2308 apply(auto) |
|
2309 apply(case_tac x) |
|
2310 apply(auto) |
|
2311 apply(case_tac x) |
|
2312 apply(auto) |
|
2313 done |
|
2314 |
|
2315 lemma flts_bsimp: |
|
2316 "flts (map bsimp rs) = map bsimp (flts rs)" |
|
2317 apply(induct rs taking: size rule: measure_induct) |
|
2318 apply(case_tac x) |
|
2319 apply(simp) |
|
2320 apply(simp) |
|
2321 apply(induct rs rule: flts.induct) |
|
2322 apply(simp) |
|
2323 apply(simp) |
|
2324 defer |
|
2325 apply(simp) |
|
2326 apply(simp) |
|
2327 defer |
|
2328 apply(simp) |
|
2329 apply(subst List.list.map(2)) |
|
2330 apply(simp only: flts.simps) |
|
2331 apply(subst k0) |
|
2332 apply(subst map_append) |
|
2333 apply(simp only:) |
|
2334 apply(simp del: bsimp.simps) |
|
2335 apply(case_tac rs1) |
|
2336 apply(simp) |
|
2337 apply(simp) |
|
2338 apply(case_tac list) |
|
2339 apply(simp_all) |
|
2340 thm map |
|
2341 apply(subst map.simps) |
|
2342 apply(auto) |
|
2343 defer |
|
2344 apply(case_tac "(bsimp va) = AZERO") |
|
2345 apply(simp) |
|
2346 |
|
2347 using b3 apply for ce |
|
2348 apply(case_tac "(bsimp a2) = AZERO") |
|
2349 apply(simp) |
|
2350 apply (me tis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1)) |
|
2351 apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs") |
|
2352 apply(clarify) |
|
2353 apply(simp) |
|
2354 |
|
2355 |
|
2356 lemma XXX: |
|
2357 shows "bsimp (bsimp a) = bsimp a" |
|
2358 sorry |
|
2359 |
|
2360 lemma bder_fuse: |
|
2361 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
|
2362 apply(induct a arbitrary: bs c) |
|
2363 apply(simp_all) |
|
2364 done |
|
2365 |
|
2366 lemma XXX2: |
|
2367 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
2368 apply(induct a arbitrary: c) |
|
2369 apply(simp) |
|
2370 apply(simp) |
|
2371 apply(simp) |
|
2372 prefer 3 |
|
2373 apply(simp) |
|
2374 apply(auto)[1] |
|
2375 apply(case_tac "(bsimp a1) = AZERO") |
|
2376 apply(simp) |
|
2377 using b3 apply force |
|
2378 apply(case_tac "(bsimp a2) = AZERO") |
|
2379 apply(simp) |
|
2380 apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1)) |
|
2381 apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs") |
|
2382 apply(clarify) |
|
2383 apply(simp) |
|
2384 apply(subst bsimp_ASEQ2) |
|
2385 apply(subgoal_tac "bmkeps a1 = bs") |
|
2386 prefer 2 |
|
2387 apply (simp add: bmkeps_simp) |
|
2388 apply(simp) |
|
2389 apply(subst (1) bsimp_fuse[symmetric]) |
|
2390 defer |
|
2391 apply(subst bsimp_ASEQ1) |
|
2392 apply(simp) |
|
2393 apply(simp) |
|
2394 apply(simp) |
|
2395 apply(auto)[1] |
|
2396 apply (metis XXX bmkeps_simp bsimp_fuse) |
|
2397 using b3 apply blast |
|
2398 apply (smt XXX b3 bder.simps(1) bder.simps(5) bnullable.simps(2) bsimp.simps(1) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1) |
|
2399 apply(simp) |
|
2400 prefer 2 |
|
2401 apply(subst bder_fuse) |
|
2402 apply(subst bsimp_fuse[symmetric]) |
|
2403 apply(simp) |
|
2404 sorry |
|
2405 |
|
2406 |
|
2407 thm bsimp_AALTs.simps |
|
2408 thm bsimp.simps |
|
2409 thm flts.simps |
|
2410 |
|
2411 lemma XXX3: |
|
2412 "bsimp (bders (bsimp r) s) = bsimp (bders r s)" |
|
2413 apply(induct s arbitrary: r rule: rev_induct) |
|
2414 apply(simp) |
|
2415 apply (simp add: XXX) |
|
2416 apply(simp add: bders_append) |
|
2417 apply(subst (2) XXX2[symmetric]) |
|
2418 apply(subst XXX2[symmetric]) |
|
2419 apply(drule_tac x="r" in meta_spec) |
|
2420 apply(simp) |
|
2421 done |
|
2422 |
|
2423 lemma XXX4: |
|
2424 "bders_simp (bsimp r) s = bsimp (bders r s)" |
|
2425 apply(induct s arbitrary: r) |
|
2426 apply(simp) |
|
2427 apply(simp) |
|
2428 by (metis XXX2) |
|
2429 |
|
2430 |
|
2431 lemma |
|
2432 assumes "bnullable (bder c r)" "bnullable (bder c (bsimp r))" |
|
2433 shows "bmkeps (bder c r) = bmkeps (bder c (bsimp r))" |
|
2434 using assms |
|
2435 apply(induct r arbitrary: c) |
|
2436 apply(simp) |
|
2437 apply(simp) |
|
2438 apply(simp) |
|
2439 prefer 3 |
|
2440 apply(simp) |
|
2441 apply(auto)[1] |
|
2442 apply(case_tac "(bsimp r1) = AZERO") |
|
2443 apply(simp) |
|
2444 apply(case_tac "(bsimp r2) = AZERO") |
|
2445 apply(simp) |
|
2446 apply (simp add: bsimp_ASEQ0) |
|
2447 apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs") |
|
2448 apply(clarify) |
|
2449 apply(simp) |
|
2450 apply(subgoal_tac "bnullable r1") |
|
2451 prefer 2 |
|
2452 using b3 apply force |
|
2453 apply(simp) |
|
2454 apply(simp add: bsimp_ASEQ2) |
|
2455 prefer 2 |
|
2456 |
|
2457 |
|
2458 |
|
2459 apply(subst bsimp_ASEQ2) |
|
2460 |
|
2461 |
|
2462 |
|
2463 |
|
2464 |
|
2465 |
|
2466 lemma |
|
2467 assumes "bnullable (bders a (s1 @ s2))" "bnullable (bders (bsimp (bders a s1)) s2)" |
|
2468 shows "bmkeps (bders a (s1 @ s2)) = bmkeps (bders (bsimp (bders a s1)) s2)" |
|
2469 using assms |
|
2470 apply(induct s2 arbitrary: a s1) |
|
2471 apply(simp) |
|
2472 using bmkeps_simp apply blast |
|
2473 apply(simp add: bders_append) |
|
2474 apply(drule_tac x="aa" in meta_spec) |
|
2475 apply(drule_tac x="s1 @ [a]" in meta_spec) |
|
2476 apply(drule meta_mp) |
|
2477 apply(simp add: bders_append) |
|
2478 apply(simp add: bders_append) |
|
2479 apply(drule meta_mp) |
|
2480 apply (metis b4 bders.simps(2) bders_simp.simps(2)) |
|
2481 apply(simp) |
|
2482 |
|
2483 apply (met is b4 bders.simps(2) bders_simp.simps(2)) |
|
2484 |
|
2485 |
|
2486 |
|
2487 using b3 apply blast |
|
2488 using b3 apply auto[1] |
|
2489 apply(auto simp add: blex_def) |
|
2490 prefer 3 |
|
2491 |
|
2492 |
1995 |
2493 |
1996 |
2494 |
1997 |
2495 |
1998 end |
2496 end |