equal
deleted
inserted
replaced
766 |
766 |
767 |
767 |
768 |
768 |
769 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where |
769 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where |
770 "star_update c r [] = []" |
770 "star_update c r [] = []" |
771 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) |
771 |"star_update c r (s # Ss) = (if (rnullable (rders r s)) |
772 then (s@[c]) # [c] # (star_update c r Ss) |
772 then (s@[c]) # [c] # (star_update c r Ss) |
773 else (s@[c]) # (star_update c r Ss) )" |
773 else (s@[c]) # (star_update c r Ss) )" |
|
774 |
774 |
775 |
775 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" |
776 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" |
776 where |
777 where |
777 "star_updates [] r Ss = Ss" |
778 "star_updates [] r Ss = Ss" |
778 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
779 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
|
780 |
|
781 lemma stupdates_append: shows |
|
782 "star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" |
|
783 apply(induct s arbitrary: Ss) |
|
784 apply simp |
|
785 apply simp |
|
786 done |
779 |
787 |
780 |
788 |
781 lemma distinct_flts_no0: |
789 lemma distinct_flts_no0: |
782 shows " rflts (map rsimp (rdistinct rs (insert RZERO rset))) = |
790 shows " rflts (map rsimp (rdistinct rs (insert RZERO rset))) = |
783 rflts (map rsimp (rdistinct rs rset)) " |
791 rflts (map rsimp (rdistinct rs rset)) " |