1262 apply(subst basic_rsimp_SEQ_property2) |
1262 apply(subst basic_rsimp_SEQ_property2) |
1263 apply simp+ |
1263 apply simp+ |
1264 apply(subgoal_tac "rnullable (rsimp r1)") |
1264 apply(subgoal_tac "rnullable (rsimp r1)") |
1265 apply simp |
1265 apply simp |
1266 using rsimp_idem apply presburger |
1266 using rsimp_idem apply presburger |
1267 |
1267 using der_simp_nullability by presburger |
|
1268 |
|
1269 |
|
1270 inductive |
|
1271 hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
|
1272 where |
|
1273 "RSEQ RZERO r2 \<leadsto> RZERO" |
|
1274 | "RSEQ r1 RZERO \<leadsto> RZERO" |
|
1275 | "RSEQ RONE r \<leadsto> r" |
|
1276 | "r1 \<leadsto> r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r2 r3" |
|
1277 | "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4" |
|
1278 | "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS (rs1 @ [r'] @ rs2))" |
|
1279 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*) |
|
1280 | "RALTS (rsa @ [AZERO] @ rsb) \<leadsto> RALTS (rsa @ rsb)" |
|
1281 | "RALTS (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)" |
|
1282 | "RALTS [] \<leadsto> RZERO" |
|
1283 | "RALTS [r] \<leadsto> r" |
|
1284 | "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)" |
|
1285 |
|
1286 inductive |
|
1287 hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
|
1288 where |
|
1289 rs1[intro, simp]:"r \<leadsto>* r" |
|
1290 | rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3" |
|
1291 |
|
1292 |
|
1293 lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2" |
|
1294 using hrewrites.intros(1) hrewrites.intros(2) by blast |
|
1295 |
|
1296 lemma hreal_trans[trans]: |
|
1297 assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3" |
|
1298 shows "r1 \<leadsto>* r3" |
|
1299 using a2 a1 |
|
1300 apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct) |
|
1301 apply(auto) |
|
1302 done |
|
1303 |
|
1304 lemma hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3" |
|
1305 by (meson hr_in_rstar hreal_trans) |
|
1306 |
|
1307 lemma hrewrites_seq_context: |
|
1308 shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3" |
|
1309 apply(induct r1 r2 rule: hrewrites.induct) |
|
1310 apply simp |
|
1311 using hrewrite.intros(4) by blast |
|
1312 |
|
1313 lemma hrewrites_seq_context2: |
|
1314 shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2" |
|
1315 apply(induct r1 r2 rule: hrewrites.induct) |
|
1316 apply simp |
|
1317 using hrewrite.intros(5) by blast |
|
1318 |
|
1319 lemma hrewrites_seq_context0: |
|
1320 shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO" |
|
1321 apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3") |
|
1322 using hrewrite.intros(1) apply blast |
|
1323 by (simp add: hrewrites_seq_context) |
|
1324 |
|
1325 lemma hrewrites_seq_contexts: |
|
1326 shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4" |
|
1327 by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) |
|
1328 |
|
1329 lemma hrewrites_simpeq: |
|
1330 shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
|
1331 sorry |
|
1332 |
|
1333 lemma distinct_grewrites_subgoal1: |
|
1334 shows " \<And>rs1 rs2 rs3 a list. |
|
1335 \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3; rs2 = [a]; list = []\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3" |
|
1336 (* apply (smt (z3) append.left_neutral append.right_neutral append_Cons grewrite.simps grewrite_singleton hrewrite.intros(10) hrewrite.intros(9) hrewrites.simps list.inject r_finite1 rsimp_ALTs.elims rsimp_ALTs.simps(2) rsimp_alts_equal)*) |
|
1337 sorry |
|
1338 |
|
1339 lemma grewrite_ralts: |
|
1340 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'" |
|
1341 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8)) |
|
1342 |
|
1343 |
|
1344 |
|
1345 |
|
1346 lemma grewrites_ralts: |
|
1347 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'" |
|
1348 apply(induct rs rs' rule: grewrites.induct) |
|
1349 apply simp |
|
1350 using grewrite_ralts hreal_trans by blast |
|
1351 |
|
1352 |
|
1353 lemma grewrites_ralts_rsimpalts: |
|
1354 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' " |
|
1355 apply(induct rs rs' rule: grewrites.induct) |
|
1356 apply(case_tac rs) |
|
1357 using hrewrite.intros(9) apply force |
|
1358 apply(case_tac list) |
|
1359 apply simp |
|
1360 using hr_in_rstar hrewrite.intros(10) rsimp_ALTs.simps(2) apply presburger |
|
1361 apply simp |
|
1362 apply(case_tac rs2) |
|
1363 apply simp |
|
1364 apply (metis grewrite.intros(3) grewrite_singleton rsimp_ALTs.simps(1)) |
|
1365 apply(case_tac list) |
|
1366 apply(simp) |
|
1367 using distinct_grewrites_subgoal1 apply blast |
|
1368 apply simp |
|
1369 apply(case_tac rs3) |
|
1370 apply simp |
|
1371 using grewrites_ralts hrewrite.intros(9) apply blast |
|
1372 by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
|
1373 |
|
1374 lemma hrewrites_list: |
|
1375 shows "\<forall>r \<in> set rs. r \<leadsto>* f r \<Longrightarrow> rs \<leadsto>g* map f rs" |
|
1376 sorry |
|
1377 |
|
1378 |
|
1379 lemma simp_hrewrites: |
|
1380 shows "r1 \<leadsto>* rsimp r1" |
|
1381 apply(induct r1) |
|
1382 apply simp+ |
|
1383 apply(case_tac "rsimp r11 = RONE") |
|
1384 apply simp |
|
1385 apply(subst basic_rsimp_SEQ_property1) |
|
1386 apply(subgoal_tac "RSEQ r11 r12 \<leadsto>* RSEQ RONE r12") |
|
1387 using hreal_trans hrewrite.intros(3) apply blast |
|
1388 using hrewrites_seq_context apply presburger |
|
1389 apply(case_tac "rsimp r11 = RZERO") |
|
1390 apply simp |
|
1391 using hrewrite.intros(1) hrewrites_seq_context apply blast |
|
1392 apply(case_tac "rsimp r12 = RZERO") |
|
1393 apply simp |
|
1394 apply(subst basic_rsimp_SEQ_property3) |
|
1395 apply (meson hrewrite.intros(2) hrewrites.simps hrewrites_seq_context2) |
|
1396 apply(subst basic_rsimp_SEQ_property2) |
|
1397 apply simp+ |
|
1398 using hrewrites_seq_contexts apply presburger |
|
1399 apply simp |
|
1400 apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)") |
|
1401 apply(subgoal_tac "RALTS (map rsimp x) \<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ") |
|
1402 using hreal_trans apply blast |
|
1403 apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct) |
|
1404 sledgehammer |
1268 sorry |
1405 sorry |
1269 |
1406 |
1270 |
1407 |
1271 lemma inside_simp_removal: |
1408 lemma inside_simp_removal: |
1272 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1409 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1392 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
1534 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
1393 apply(induct s) |
1535 apply(induct s) |
1394 apply simp |
1536 apply simp |
1395 sorry |
1537 sorry |
1396 |
1538 |
1397 |
1539 thm vsuf.simps |
|
1540 |
|
1541 |
|
1542 |
|
1543 lemma rsimp_seq_equal1: |
|
1544 shows "rsimp_SEQ (rsimp r1) (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp r1) (rsimp r2)]) {})" |
|
1545 by (metis idem_after_simp1 rsimp.simps(1)) |
|
1546 |
|
1547 |
|
1548 |
|
1549 lemma vsuf_der_stepwise: |
|
1550 shows "rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1))) = |
|
1551 rsimp (rder x (rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # map (rders_simp r2) (vsuf xs r1)))))" |
|
1552 apply simp |
|
1553 apply(subst rders_simp_append) |
|
1554 |
|
1555 oops |
|
1556 |
|
1557 fun sflat :: "rrexp \<Rightarrow> rrexp list " where |
|
1558 "sflat (RALT r1 r2) = sflat r1 @ [r2]" |
|
1559 | "sflat (RALTS rs) = rs" |
|
1560 | "sflat r = [r]" |
|
1561 |
|
1562 lemma seq_sflat0: |
|
1563 shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) # |
|
1564 (map (rders r2) (vsuf s r1))) )" |
|
1565 |
|
1566 sorry |
|
1567 |
|
1568 lemma seq_sflat1: |
|
1569 shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # |
|
1570 (map (rders r2) (vsuf (s @ [c]) r1)) |
|
1571 ) ) = sflat (rders (RSEQ r1 r2) (s @ [c]))" |
|
1572 sorry |
|
1573 |
|
1574 |
|
1575 lemma seq_sflat: |
|
1576 shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # |
|
1577 (map (rders r2) (vsuf (s @ [c]) r1)) |
|
1578 ) ) = sflat ( rder x (RALTS ( (RSEQ (rders r1 s) r2) # |
|
1579 (map (rders r2) (vsuf s r1)) |
|
1580 )) )" |
|
1581 sorry |
|
1582 |
|
1583 |
|
1584 |
|
1585 lemma sflat_rsimpeq: |
|
1586 shows "sflat r1 = sflat r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
|
1587 sorry |
|
1588 |
|
1589 |
|
1590 |
|
1591 lemma seq_closed_form_general: |
|
1592 shows "rsimp (rders (RSEQ r1 r2) s) = |
|
1593 rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
|
1594 apply(subgoal_tac "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))") |
|
1595 using sflat_rsimpeq apply blast |
|
1596 by (simp add: seq_sflat0) |
|
1597 |
|
1598 lemma seq_closed_form_aux1: |
|
1599 shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) = |
|
1600 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
|
1601 by (smt (verit, best) list.simps(9) rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders rsimp.simps(1) rsimp.simps(2) rsimp_idem) |
|
1602 |
|
1603 lemma add_simp_to_rest: |
|
1604 shows "rsimp (RALTS (r # rs)) = rsimp (RALTS (r # map rsimp rs))" |
|
1605 by (metis append_Nil2 grewrite.intros(2) grewrite_simpalts head_one_more_simp list.simps(9) rsimp_ALTs.simps(2) spawn_simp_rsimpalts) |
|
1606 |
|
1607 lemma rsimp_compose_der: |
|
1608 shows "map rsimp (map (rders r) ss) = map (\<lambda>s. rsimp (rders r s)) ss" |
|
1609 apply simp |
|
1610 done |
|
1611 |
|
1612 lemma rsimp_compose_der2: |
|
1613 shows "\<forall>s \<in> set ss. s \<noteq> [] \<Longrightarrow> map rsimp (map (rders r) ss) = map (\<lambda>s. (rders_simp r s)) ss" |
|
1614 by (simp add: rders_simp_same_simpders) |
|
1615 |
|
1616 lemma vsuf_nonempty: |
|
1617 shows "\<forall>s \<in> set ( vsuf s1 r). s \<noteq> []" |
|
1618 apply(induct s1 arbitrary: r) |
|
1619 apply simp |
|
1620 apply simp |
|
1621 done |
|
1622 |
|
1623 lemma rsimp_compose_der3: |
|
1624 shows " map rsimp (map (rders r) (vsuf s1 r')) = map (\<lambda>s. rsimp (rders_simp r s)) (vsuf s1 r')" |
|
1625 by (simp add: rders_simp_same_simpders rsimp_idem vsuf_nonempty) |
|
1626 |
|
1627 thm rders_simp_same_simpders |
|
1628 |
|
1629 |
|
1630 |
|
1631 lemma seq_closed_form_aux2: |
|
1632 shows "s \<noteq> [] \<Longrightarrow> rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1)))))) = |
|
1633 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))))" |
|
1634 |
|
1635 by (metis add_simp_to_rest rsimp_compose_der2 vsuf_nonempty) |
|
1636 |
1398 |
1637 |
1399 lemma seq_closed_form: shows |
1638 lemma seq_closed_form: shows |
1400 "rsimp (rders_simp (RSEQ r1 r2) s) = |
1639 "rsimp (rders_simp (RSEQ r1 r2) s) = |
1401 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # |
1640 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # |
1402 (map (rders_simp r2) (vsuf s r1)) |
1641 (map (rders_simp r2) (vsuf s r1)) |
1403 ) |
1642 ) |
1404 )" |
1643 )" |
1405 apply(induct s) |
1644 apply(case_tac s ) |
1406 apply simp |
1645 apply simp |
1407 sorry |
1646 apply (metis idem_after_simp1 rsimp.simps(1)) |
|
1647 apply(subgoal_tac " s \<noteq> []") |
|
1648 using rders_simp_same_simpders rsimp_idem seq_closed_form_aux1 seq_closed_form_aux2 seq_closed_form_general apply presburger |
|
1649 |
|
1650 by fastforce |
|
1651 |
|
1652 |
|
1653 |
1408 |
1654 |
1409 |
1655 |
1410 lemma seq_closed_form_variant: shows |
1656 lemma seq_closed_form_variant: shows |
1411 "s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) = |
1657 "s \<noteq> [] \<Longrightarrow> (rders_simp (RSEQ r1 r2) s) = |
1412 rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))" |
1658 rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))" |