equal
deleted
inserted
replaced
64 by (simp add: Pi_def) |
64 by (simp add: Pi_def) |
65 |
65 |
66 lemma PiE [elim]: |
66 lemma PiE [elim]: |
67 "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q" |
67 "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q" |
68 by(auto simp: Pi_def) |
68 by(auto simp: Pi_def) |
|
69 |
|
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" |
|
72 by (auto simp: Pi_def) |
69 |
73 |
70 lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" |
74 lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A" |
71 by (auto intro: Pi_I) |
75 by (auto intro: Pi_I) |
72 |
76 |
73 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" |