equal
deleted
inserted
replaced
381 |
381 |
382 lemma bexE [elim!]: "\<exists>x\<in>A. P x \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P x \<Longrightarrow> Q) \<Longrightarrow> Q" |
382 lemma bexE [elim!]: "\<exists>x\<in>A. P x \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P x \<Longrightarrow> Q) \<Longrightarrow> Q" |
383 unfolding Bex_def by blast |
383 unfolding Bex_def by blast |
384 |
384 |
385 lemma ball_triv [simp]: "(\<forall>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<longrightarrow> P)" |
385 lemma ball_triv [simp]: "(\<forall>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<longrightarrow> P)" |
386 \<comment> \<open>Trival rewrite rule.\<close> |
386 \<comment> \<open>trivial rewrite rule.\<close> |
387 by (simp add: Ball_def) |
387 by (simp add: Ball_def) |
388 |
388 |
389 lemma bex_triv [simp]: "(\<exists>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<and> P)" |
389 lemma bex_triv [simp]: "(\<exists>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<and> P)" |
390 \<comment> \<open>Dual form for existentials.\<close> |
390 \<comment> \<open>Dual form for existentials.\<close> |
391 by (simp add: Bex_def) |
391 by (simp add: Bex_def) |