added simp rule
authornipkow
Sun, 17 Jun 2018 13:10:14 +0200
changeset 68457 517aa9076fc9
parent 68456 ba2a92af88b4
child 68458 b047339bd11c
child 68460 0eb751466b79
added simp rule
src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Jun 16 22:09:24 2018 +0200
+++ b/src/HOL/Product_Type.thy	Sun Jun 17 13:10:14 2018 +0200
@@ -670,6 +670,9 @@
 lemma pair_imageI [intro]: "(a, b) \<in> A \<Longrightarrow> f a b \<in> (\<lambda>(a, b). f a b) ` A"
   by (rule image_eqI [where x = "(a, b)"]) auto
 
+lemma Collect_const_case_prod[simp]: "{(a,b). P} = (if P then UNIV else {})"
+by auto
+
 lemma The_split_eq [simp]: "(THE (x',y'). x = x' \<and> y = y') = (x, y)"
   by blast