add lemmas about bind and image
authorAndreas Lochbihler
Wed Feb 11 13:47:48 2015 +0100 (2015-02-11)
changeset 595129bf568cc71a4
parent 59507 b468e0f8da2a
child 59513 6949c8837e90
add lemmas about bind and image
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Wed Feb 11 12:01:56 2015 +0000
     1.2 +++ b/src/HOL/Fun.thy	Wed Feb 11 13:47:48 2015 +0100
     1.3 @@ -88,6 +88,12 @@
     1.4  lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h o f) ` A = (h o g) ` B"
     1.5    by (auto simp: comp_def elim!: equalityE)
     1.6  
     1.7 +lemma image_bind: "f ` (Set.bind A g) = Set.bind A (op ` f \<circ> g)"
     1.8 +by(auto simp add: Set.bind_def)
     1.9 +
    1.10 +lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \<circ> f)"
    1.11 +by(auto simp add: Set.bind_def)
    1.12 +
    1.13  code_printing
    1.14    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    1.15