src/HOL/Basic_BNFs.thy
changeset 55932 68c5104d2204
parent 55931 62156e694f3d
child 55935 8f20d09d294e
     1.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:15 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:48 2014 +0100
     1.3 @@ -129,27 +129,27 @@
     1.4    by (simp add: prod_rel_def)
     1.5  
     1.6  bnf "'a \<times> 'b"
     1.7 -  map: map_pair
     1.8 +  map: map_prod
     1.9    sets: fsts snds
    1.10    bd: natLeq
    1.11    rel: prod_rel
    1.12  proof (unfold prod_set_defs)
    1.13 -  show "map_pair id id = id" by (rule map_pair.id)
    1.14 +  show "map_prod id id = id" by (rule map_prod.id)
    1.15  next
    1.16    fix f1 f2 g1 g2
    1.17 -  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
    1.18 -    by (rule map_pair.comp[symmetric])
    1.19 +  show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
    1.20 +    by (rule map_prod.comp[symmetric])
    1.21  next
    1.22    fix x f1 f2 g1 g2
    1.23    assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
    1.24 -  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
    1.25 +  thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
    1.26  next
    1.27    fix f1 f2
    1.28 -  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
    1.29 +  show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
    1.30      by (rule ext, unfold o_apply) simp
    1.31  next
    1.32    fix f1 f2
    1.33 -  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
    1.34 +  show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
    1.35      by (rule ext, unfold o_apply) simp
    1.36  next
    1.37    show "card_order natLeq" by (rule natLeq_card_order)
    1.38 @@ -169,8 +169,8 @@
    1.39  next
    1.40    fix R S
    1.41    show "prod_rel R S =
    1.42 -        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
    1.43 -        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
    1.44 +        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
    1.45 +        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
    1.46    unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    1.47    by auto
    1.48  qed