# HG changeset patch
# User Andreas Lochbihler
# Date 1423658868 -3600
# Node ID 9bf568cc71a48f7356ba254c737c680715669e98
# Parent  b468e0f8da2adb0bc9d080d6ab29263dbc976a4e
add lemmas about bind and image

diff -r b468e0f8da2a -r 9bf568cc71a4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Feb 11 12:01:56 2015 +0000
+++ b/src/HOL/Fun.thy	Wed Feb 11 13:47:48 2015 +0100
@@ -88,6 +88,12 @@
 lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h o f) ` A = (h o g) ` B"
   by (auto simp: comp_def elim!: equalityE)
 
+lemma image_bind: "f ` (Set.bind A g) = Set.bind A (op ` f \<circ> g)"
+by(auto simp add: Set.bind_def)
+
+lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \<circ> f)"
+by(auto simp add: Set.bind_def)
+
 code_printing
   constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."