equal
deleted
inserted
replaced
136 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
136 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
137 by auto |
137 by auto |
138 |
138 |
139 lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)" |
139 lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)" |
140 apply (induct xs) |
140 apply (induct xs) |
141 apply (metis map.simps(1) zip_Nil) |
141 apply (metis list.map(1) zip_Nil) |
142 by auto |
142 by auto |
143 |
143 |
144 lemma |
144 lemma |
145 "map (\<lambda>w. (w -> w, w \<times> w)) xs = |
145 "map (\<lambda>w. (w -> w, w \<times> w)) xs = |
146 zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)" |
146 zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)" |
147 apply (induct xs) |
147 apply (induct xs) |
148 apply (metis map.simps(1) zip_Nil) |
148 apply (metis list.map(1) zip_Nil) |
149 by auto |
149 by auto |
150 |
150 |
151 lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A" |
151 lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A" |
152 by (metis mem_Collect_eq image_eqI subsetD) |
152 by (metis mem_Collect_eq image_eqI subsetD) |
153 |
153 |