# HG changeset patch
# User nipkow
# Date 1540102746 -7200
# Node ID 6c9453ec2191ffe13f33721960740316987a6ed5
# Parent  88842948515b515c103b9f2b7fff46eea5a4d656
added lemma

diff -r 88842948515b -r 6c9453ec2191 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Oct 20 15:36:32 2018 +0200
+++ b/src/HOL/Set.thy	Sun Oct 21 08:19:06 2018 +0200
@@ -936,8 +936,11 @@
   "(\<lambda>x. if P x then f x else g x) ` S = f ` (S \<inter> {x. P x}) \<union> g ` (S \<inter> {x. \<not> P x})"
   by auto
 
-lemma image_cong: "M = N \<Longrightarrow> (\<And>x. x \<in> N \<Longrightarrow> f x = g x) \<Longrightarrow> f ` M = g ` N"
-  by (simp add: image_def)
+lemma image_cong: "\<lbrakk> M = N;  \<And>x. x \<in> N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> f ` M = g ` N"
+by (simp add: image_def)
+
+lemma image_cong_strong: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
+by (simp add: image_def simp_implies_def)
 
 lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
   by blast