1524 *) |
1524 *) |
1525 |
1525 |
1526 |
1526 |
1527 lemma hfau_pushin: |
1527 lemma hfau_pushin: |
1528 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" |
1528 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" |
1529 apply(induct r rule: created_by_star.induct) |
1529 |
1530 apply simp |
1530 proof(induct r rule: created_by_star.induct) |
1531 apply(subgoal_tac "created_by_star (rder c r1)") |
1531 case (1 ra rb) |
1532 prefer 2 |
1532 then show ?case by simp |
1533 apply(subgoal_tac "created_by_star (rder c r2)") |
1533 next |
1534 using cbs_ders_cbs apply blast |
1534 case (2 r1 r2) |
1535 using cbs_ders_cbs apply auto[1] |
1535 then have "created_by_star (rder c r1)" |
1536 apply simp |
1536 using cbs_ders_cbs by blast |
1537 done |
1537 then have "created_by_star (rder c r2)" |
|
1538 using "2.hyps"(3) cbs_ders_cbs by auto |
|
1539 then show ?case |
|
1540 apply simp |
|
1541 by (simp add: "2.hyps"(2) "2.hyps"(4)) |
|
1542 qed |
|
1543 |
|
1544 |
1538 |
1545 |
1539 lemma stupdate_induct1: |
1546 lemma stupdate_induct1: |
1540 shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = |
1547 shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = |
1541 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" |
1548 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" |
1542 apply(induct Ss) |
1549 apply(induct Ss) |
1604 by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites) |
1611 by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites) |
1605 |
1612 |
1606 |
1613 |
1607 lemma hfau_rsimpeq2: |
1614 lemma hfau_rsimpeq2: |
1608 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
1615 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
|
1616 apply(induct rule: created_by_star.induct) |
|
1617 apply simp |
|
1618 apply (metis rsimp.simps(6) rsimp_seq_equal1) |
|
1619 using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger |
|
1620 |
|
1621 |
|
1622 (* |
|
1623 lemma hfau_rsimpeq2_oldproof: shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
1609 apply(induct r) |
1624 apply(induct r) |
1610 apply simp+ |
1625 apply simp+ |
1611 |
|
1612 apply (metis rsimp_seq_equal1) |
1626 apply (metis rsimp_seq_equal1) |
1613 prefer 2 |
1627 prefer 2 |
1614 apply simp |
1628 apply simp |
1615 apply(case_tac x) |
1629 apply(case_tac x) |
1616 apply simp |
1630 apply simp |
1617 apply(case_tac "list") |
1631 apply(case_tac "list") |
1618 apply simp |
1632 apply simp |
1619 |
|
1620 apply (metis idem_after_simp1) |
1633 apply (metis idem_after_simp1) |
1621 apply(case_tac "lista") |
1634 apply(case_tac "lista") |
1622 prefer 2 |
1635 prefer 2 |
1623 apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) |
1636 apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) |
1624 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") |
1637 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") |
1625 apply simp |
1638 apply simp |
1626 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") |
1639 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") |
1627 using hflat_aux.simps(1) apply presburger |
1640 using hflat_aux.simps(1) apply presburger |
1628 apply simp |
1641 apply simp |
1629 using cbs_hfau_rsimpeq1 by fastforce |
1642 using cbs_hfau_rsimpeq1 by fastforce |
|
1643 *) |
1630 |
1644 |
1631 lemma star_closed_form1: |
1645 lemma star_closed_form1: |
1632 shows "rsimp (rders (RSTAR r0) (c#s)) = |
1646 shows "rsimp (rders (RSTAR r0) (c#s)) = |
1633 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
1647 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
1634 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger |
1648 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger |