thys2/BasicIdentities.thy
changeset 486 f5b96a532c85
parent 481 feacb89b784c
child 488 370dae790b30
equal deleted inserted replaced
485:72edbac05c59 486:f5b96a532c85
   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))  "