equal
deleted
inserted
replaced
205 done |
205 done |
206 |
206 |
207 lemma fsfilter_fscons: |
207 lemma fsfilter_fscons: |
208 "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" |
208 "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" |
209 apply (unfold fsfilter_def) |
209 apply (unfold fsfilter_def) |
210 apply (simp add: fscons_def2 sfilter_scons If_and_if) |
210 apply (simp add: fscons_def2 If_and_if) |
211 done |
211 done |
212 |
212 |
213 lemma fsfilter_emptys: "{}(C)x = UU" |
213 lemma fsfilter_emptys: "{}(C)x = UU" |
214 apply (rule_tac x="x" in fstream_ind) |
214 apply (rule_tac x="x" in fstream_ind) |
215 apply (simp) |
215 apply (simp) |