equal
deleted
inserted
replaced
268 lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F" |
268 lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F" |
269 using [[simp_depth_limit = 2]] |
269 using [[simp_depth_limit = 2]] |
270 by (auto simp add: Fun_def Sep Domain) |
270 by (auto simp add: Fun_def Sep Domain) |
271 |
271 |
272 |
272 |
273 lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f" |
273 lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> \<exists>!y. Elem (Opair x y) f" |
274 by (auto simp add: Domain isFun_def) |
274 by (auto simp add: Domain isFun_def) |
275 |
275 |
276 lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)" |
276 lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)" |
277 apply (auto simp add: Range) |
277 apply (auto simp add: Range) |
278 apply (drule unique_fun_value) |
278 apply (drule unique_fun_value) |