# HG changeset patch
# User nipkow
# Date 1529233814 -7200
# Node ID 517aa9076fc93bd3fe27e5fb0299c1eb1b8a3a3c
# Parent  ba2a92af88b428458fe1ac766cc6360549a695ed
added simp rule

diff -r ba2a92af88b4 -r 517aa9076fc9 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