src/HOL/Set.thy
changeset 46036 6a86cc88b02f
parent 46026 83caa4f4bd56
child 46127 af3b95160b59
     1.1 --- a/src/HOL/Set.thy	Thu Dec 29 14:44:44 2011 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Dec 29 14:23:40 2011 +0100
     1.3 @@ -1790,6 +1790,22 @@
     1.4  
     1.5  hide_const (open) bind
     1.6  
     1.7 +lemma bind_bind:
     1.8 +  fixes A :: "'a set"
     1.9 +  shows "Set.bind (Set.bind A B) C = Set.bind A (\<lambda>x. Set.bind (B x) C)"
    1.10 +  by (auto simp add: bind_def)
    1.11 +
    1.12 +lemma empty_bind [simp]:
    1.13 +  "Set.bind {} B = {}"
    1.14 +  by (simp add: bind_def)
    1.15 +
    1.16 +lemma nonempty_bind_const:
    1.17 +  "A \<noteq> {} \<Longrightarrow> Set.bind A (\<lambda>_. B) = B"
    1.18 +  by (auto simp add: bind_def)
    1.19 +
    1.20 +lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
    1.21 +  by (auto simp add: bind_def)
    1.22 +
    1.23  
    1.24  subsubsection {* Operations for execution *}
    1.25