src/HOL/BNF_FP_Base.thy
changeset 55414 eab03e9cee8a
parent 55083 0a689157e3ce
child 55538 6a5986170c1d
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -19,10 +19,10 @@
     1.4  lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
     1.5  by blast
     1.6  
     1.7 -lemma unit_case_Unity: "(case u of () \<Rightarrow> f) = f"
     1.8 +lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
     1.9  by (cases u) (hypsubst, rule unit.cases)
    1.10  
    1.11 -lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    1.12 +lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    1.13  by simp
    1.14  
    1.15  lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
    1.16 @@ -53,9 +53,9 @@
    1.17  
    1.18  lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
    1.19  
    1.20 -lemma sum_case_step:
    1.21 -"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
    1.22 -"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
    1.23 +lemma case_sum_step:
    1.24 +"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
    1.25 +"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
    1.26  by auto
    1.27  
    1.28  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.29 @@ -71,8 +71,8 @@
    1.30  lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.31  by (cases s) auto
    1.32  
    1.33 -lemma sum_case_if:
    1.34 -"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    1.35 +lemma case_sum_if:
    1.36 +"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    1.37  by simp
    1.38  
    1.39  lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
    1.40 @@ -122,14 +122,14 @@
    1.41  lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    1.42    unfolding map_pair_o_convol id_comp comp_id ..
    1.43  
    1.44 -lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
    1.45 +lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
    1.46    unfolding comp_def by (auto split: sum.splits)
    1.47  
    1.48 -lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
    1.49 +lemma case_sum_o_sum_map: "case_sum f g o sum_map h1 h2 = case_sum (f o h1) (g o h2)"
    1.50    unfolding comp_def by (auto split: sum.splits)
    1.51  
    1.52 -lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
    1.53 -  unfolding sum_case_o_sum_map id_comp comp_id ..
    1.54 +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.55 +  unfolding case_sum_o_sum_map id_comp comp_id ..
    1.56  
    1.57  lemma fun_rel_def_butlast:
    1.58    "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"