885 lemma rders_simp_nonempty_simped: |
885 lemma rders_simp_nonempty_simped: |
886 shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)" |
886 shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)" |
887 using rders_simp_same_simpders rsimp_idem by auto |
887 using rders_simp_same_simpders rsimp_idem by auto |
888 |
888 |
889 lemma repeated_altssimp: |
889 lemma repeated_altssimp: |
890 shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) = |
890 shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> |
|
891 rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) = |
891 rsimp_ALTs (rdistinct (rflts rs) {})" |
892 rsimp_ALTs (rdistinct (rflts rs) {})" |
892 by (metis map_idI rsimp.simps(2) rsimp_idem) |
893 by (metis map_idI rsimp.simps(2) rsimp_idem) |
893 |
894 |
894 |
895 |
895 |
896 |
896 lemma alts_closed_form: |
897 lemma alts_closed_form: |
897 shows "rsimp (rders_simp (RALTS rs) s) = rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
898 shows "rsimp (rders_simp (RALTS rs) s) = |
|
899 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
898 apply(induct s rule: rev_induct) |
900 apply(induct s rule: rev_induct) |
899 apply simp |
901 apply simp |
900 apply simp |
902 apply simp |
901 apply(subst rders_simp_append) |
903 apply(subst rders_simp_append) |
902 apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) = |
904 apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) = |