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.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
```