src/HOL/Basic_BNFs.thy
changeset 55931 62156e694f3d
parent 55811 aa1acc25126b
child 55932 68c5104d2204
     1.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 12:17:26 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:15 2014 +0100
     1.3 @@ -53,22 +53,22 @@
     1.4    unfolding sum_rel_def by simp_all
     1.5  
     1.6  bnf "'a + 'b"
     1.7 -  map: sum_map
     1.8 +  map: map_sum
     1.9    sets: setl setr
    1.10    bd: natLeq
    1.11    wits: Inl Inr
    1.12    rel: sum_rel
    1.13  proof -
    1.14 -  show "sum_map id id = id" by (rule sum_map.id)
    1.15 +  show "map_sum id id = id" by (rule map_sum.id)
    1.16  next
    1.17    fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
    1.18 -  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
    1.19 -    by (rule sum_map.comp[symmetric])
    1.20 +  show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
    1.21 +    by (rule map_sum.comp[symmetric])
    1.22  next
    1.23    fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
    1.24    assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
    1.25           a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
    1.26 -  thus "sum_map f1 f2 x = sum_map g1 g2 x"
    1.27 +  thus "map_sum f1 f2 x = map_sum g1 g2 x"
    1.28    proof (cases x)
    1.29      case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
    1.30    next
    1.31 @@ -76,11 +76,11 @@
    1.32    qed
    1.33  next
    1.34    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    1.35 -  show "setl o sum_map f1 f2 = image f1 o setl"
    1.36 +  show "setl o map_sum f1 f2 = image f1 o setl"
    1.37      by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
    1.38  next
    1.39    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    1.40 -  show "setr o sum_map f1 f2 = image f2 o setr"
    1.41 +  show "setr o map_sum f1 f2 = image f2 o setr"
    1.42      by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
    1.43  next
    1.44    show "card_order natLeq" by (rule natLeq_card_order)
    1.45 @@ -105,8 +105,8 @@
    1.46  next
    1.47    fix R S
    1.48    show "sum_rel R S =
    1.49 -        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
    1.50 -        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
    1.51 +        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
    1.52 +        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
    1.53    unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    1.54    by (fastforce split: sum.splits)
    1.55  qed (auto simp: sum_set_defs)