src/HOL/BNF_FP_Base.thy
changeset 55931 62156e694f3d
parent 55930 25a90cebbbe5
child 55932 68c5104d2204
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 12:17:26 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 13:36:15 2014 +0100
     1.3 @@ -125,11 +125,11 @@
     1.4  lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
     1.5    unfolding comp_def by (auto split: sum.splits)
     1.6  
     1.7 -lemma case_sum_o_sum_map: "case_sum f g o sum_map h1 h2 = case_sum (f o h1) (g o h2)"
     1.8 +lemma case_sum_o_map_sum: "case_sum f g o map_sum h1 h2 = case_sum (f o h1) (g o h2)"
     1.9    unfolding comp_def by (auto split: sum.splits)
    1.10  
    1.11 -lemma case_sum_o_sum_map_id: "(case_sum id g o sum_map f id) x = case_sum (f o id) g x"
    1.12 -  unfolding case_sum_o_sum_map id_comp comp_id ..
    1.13 +lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x"
    1.14 +  unfolding case_sum_o_map_sum id_comp comp_id ..
    1.15  
    1.16  lemma fun_rel_def_butlast:
    1.17    "fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"