equal
deleted
inserted
replaced
70 lemma Pi_cong: |
70 lemma Pi_cong: |
71 "(\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B" |
71 "(\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B" |
72 by (auto simp: Pi_def) |
72 by (auto simp: Pi_def) |
73 |
73 |
74 lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" |
74 lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" |
75 by (auto intro: Pi_I) |
75 by auto |
76 |
76 |
77 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B" |
77 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B" |
78 by (simp add: Pi_def) |
78 by (simp add: Pi_def) |
79 |
79 |
80 lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B" |
80 lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B" |
255 |
255 |
256 definition extensional_funcset |
256 definition extensional_funcset |
257 where "extensional_funcset S T = (S -> T) \<inter> (extensional S)" |
257 where "extensional_funcset S T = (S -> T) \<inter> (extensional S)" |
258 |
258 |
259 lemma extensional_empty[simp]: "extensional {} = {%x. undefined}" |
259 lemma extensional_empty[simp]: "extensional {} = {%x. undefined}" |
260 unfolding extensional_def by (auto intro: ext) |
260 unfolding extensional_def by auto |
261 |
261 |
262 lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}" |
262 lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}" |
263 unfolding extensional_funcset_def by simp |
263 unfolding extensional_funcset_def by simp |
264 |
264 |
265 lemma extensional_funcset_empty_range: |
265 lemma extensional_funcset_empty_range: |