src/HOL/Product_Type.thy
changeset 26588 d83271bfaba5
parent 26480 544cef16045b
child 26798 a9134a089106
     1.1 --- a/src/HOL/Product_Type.thy	Wed Apr 09 08:10:09 2008 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 09 08:10:11 2008 +0200
     1.3 @@ -699,34 +699,33 @@
     1.4    The composition-uncurry combinator.
     1.5  *}
     1.6  
     1.7 -definition
     1.8 -  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o->" 60)
     1.9 -where
    1.10 -  "f o-> g = (\<lambda>x. split g (f x))"
    1.11 +notation fcomp (infixl "o>" 60)
    1.12  
    1.13 -notation (xsymbols)
    1.14 -  mbind  (infixl "\<circ>\<rightarrow>" 60)
    1.15 +definition
    1.16 +  scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60)
    1.17 +where
    1.18 +  "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
    1.19  
    1.20 -notation (HTML output)
    1.21 -  mbind  (infixl "\<circ>\<rightarrow>" 60)
    1.22 +lemma scomp_apply:  "(f o\<rightarrow> g) x = split g (f x)"
    1.23 +  by (simp add: scomp_def)
    1.24  
    1.25 -lemma mbind_apply:  "(f \<circ>\<rightarrow> g) x = split g (f x)"
    1.26 -  by (simp add: mbind_def)
    1.27 +lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
    1.28 +  by (simp add: expand_fun_eq scomp_apply)
    1.29  
    1.30 -lemma Pair_mbind: "Pair x \<circ>\<rightarrow> f = f x"
    1.31 -  by (simp add: expand_fun_eq mbind_apply)
    1.32 +lemma scomp_Pair: "x o\<rightarrow> Pair = x"
    1.33 +  by (simp add: expand_fun_eq scomp_apply)
    1.34  
    1.35 -lemma mbind_Pair: "x \<circ>\<rightarrow> Pair = x"
    1.36 -  by (simp add: expand_fun_eq mbind_apply)
    1.37 +lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
    1.38 +  by (simp add: expand_fun_eq split_twice scomp_def)
    1.39  
    1.40 -lemma mbind_mbind: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
    1.41 -  by (simp add: expand_fun_eq split_twice mbind_def)
    1.42 +lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
    1.43 +  by (simp add: expand_fun_eq scomp_apply fcomp_def split_def)
    1.44  
    1.45 -lemma mbind_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
    1.46 -  by (simp add: expand_fun_eq mbind_apply fcomp_def split_def)
    1.47 +lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
    1.48 +  by (simp add: expand_fun_eq scomp_apply fcomp_apply)
    1.49  
    1.50 -lemma fcomp_mbind: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
    1.51 -  by (simp add: expand_fun_eq mbind_apply fcomp_apply)
    1.52 +no_notation fcomp (infixl "o>" 60)
    1.53 +no_notation scomp (infixl "o\<rightarrow>" 60)
    1.54  
    1.55  
    1.56  text {*