equal
deleted
inserted
replaced
68 sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
68 sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
69 where |
69 where |
70 sfilter_nil: "sfilter$P$nil=nil" |
70 sfilter_nil: "sfilter$P$nil=nil" |
71 | sfilter_cons: |
71 | sfilter_cons: |
72 "x~=UU ==> sfilter$P$(x##xs)= |
72 "x~=UU ==> sfilter$P$(x##xs)= |
73 (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)" |
73 (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)" |
74 |
74 |
75 lemma sfilter_UU [simp]: "sfilter$P$UU=UU" |
75 lemma sfilter_UU [simp]: "sfilter$P$UU=UU" |
76 by fixrec_simp |
76 by fixrec_simp |
77 |
77 |
78 subsubsection {* sforall2 *} |
78 subsubsection {* sforall2 *} |
96 stakewhile :: "('a -> tr) -> 'a seq -> 'a seq" |
96 stakewhile :: "('a -> tr) -> 'a seq -> 'a seq" |
97 where |
97 where |
98 stakewhile_nil: "stakewhile$P$nil=nil" |
98 stakewhile_nil: "stakewhile$P$nil=nil" |
99 | stakewhile_cons: |
99 | stakewhile_cons: |
100 "x~=UU ==> stakewhile$P$(x##xs) = |
100 "x~=UU ==> stakewhile$P$(x##xs) = |
101 (If P$x then x##(stakewhile$P$xs) else nil fi)" |
101 (If P$x then x##(stakewhile$P$xs) else nil)" |
102 |
102 |
103 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" |
103 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" |
104 by fixrec_simp |
104 by fixrec_simp |
105 |
105 |
106 subsubsection {* sdropwhile *} |
106 subsubsection {* sdropwhile *} |
109 sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq" |
109 sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq" |
110 where |
110 where |
111 sdropwhile_nil: "sdropwhile$P$nil=nil" |
111 sdropwhile_nil: "sdropwhile$P$nil=nil" |
112 | sdropwhile_cons: |
112 | sdropwhile_cons: |
113 "x~=UU ==> sdropwhile$P$(x##xs) = |
113 "x~=UU ==> sdropwhile$P$(x##xs) = |
114 (If P$x then sdropwhile$P$xs else x##xs fi)" |
114 (If P$x then sdropwhile$P$xs else x##xs)" |
115 |
115 |
116 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" |
116 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" |
117 by fixrec_simp |
117 by fixrec_simp |
118 |
118 |
119 subsubsection {* slast *} |
119 subsubsection {* slast *} |
121 fixrec |
121 fixrec |
122 slast :: "'a seq -> 'a" |
122 slast :: "'a seq -> 'a" |
123 where |
123 where |
124 slast_nil: "slast$nil=UU" |
124 slast_nil: "slast$nil=UU" |
125 | slast_cons: |
125 | slast_cons: |
126 "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)" |
126 "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)" |
127 |
127 |
128 lemma slast_UU [simp]: "slast$UU=UU" |
128 lemma slast_UU [simp]: "slast$UU=UU" |
129 by fixrec_simp |
129 by fixrec_simp |
130 |
130 |
131 subsubsection {* sconc *} |
131 subsubsection {* sconc *} |