src/HOL/Product_Type.thy
changeset 37751 89e16802b6cc
parent 37704 c6161bee8486
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/Product_Type.thy	Thu Jul 08 17:23:05 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Jul 09 08:11:10 2010 +0200
     1.3 @@ -791,37 +791,37 @@
     1.4    The composition-uncurry combinator.
     1.5  *}
     1.6  
     1.7 -notation fcomp (infixl "o>" 60)
     1.8 +notation fcomp (infixl "\<circ>>" 60)
     1.9  
    1.10 -definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
    1.11 -  "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
    1.12 +definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
    1.13 +  "f \<circ>\<rightarrow> g = (\<lambda>x. prod_case g (f x))"
    1.14  
    1.15  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
    1.16 -  by (simp add: expand_fun_eq scomp_def split_def)
    1.17 +  by (simp add: expand_fun_eq scomp_def prod_case_unfold)
    1.18  
    1.19 -lemma scomp_apply:  "(f o\<rightarrow> g) x = split g (f x)"
    1.20 -  by (simp add: scomp_unfold split_def)
    1.21 +lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
    1.22 +  by (simp add: scomp_unfold prod_case_unfold)
    1.23  
    1.24 -lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
    1.25 +lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
    1.26    by (simp add: expand_fun_eq scomp_apply)
    1.27  
    1.28 -lemma scomp_Pair: "x o\<rightarrow> Pair = x"
    1.29 +lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
    1.30    by (simp add: expand_fun_eq scomp_apply)
    1.31  
    1.32 -lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
    1.33 +lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
    1.34    by (simp add: expand_fun_eq scomp_unfold)
    1.35  
    1.36 -lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
    1.37 +lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
    1.38    by (simp add: expand_fun_eq scomp_unfold fcomp_def)
    1.39  
    1.40 -lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
    1.41 +lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
    1.42    by (simp add: expand_fun_eq scomp_unfold fcomp_apply)
    1.43  
    1.44  code_const scomp
    1.45    (Eval infixl 3 "#->")
    1.46  
    1.47 -no_notation fcomp (infixl "o>" 60)
    1.48 -no_notation scomp (infixl "o\<rightarrow>" 60)
    1.49 +no_notation fcomp (infixl "\<circ>>" 60)
    1.50 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.51  
    1.52  text {*
    1.53    @{term prod_fun} --- action of the product functor upon