src/HOL/Basic_BNFs.thy
changeset 55944 7ab8f003fe41
parent 55943 5c2df04e97d1
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:25:21 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 15:29:18 2014 +0100
     1.3 @@ -104,19 +104,19 @@
     1.4  lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
     1.5  
     1.6  definition
     1.7 -  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
     1.8 +  rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
     1.9  where
    1.10 -  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.11 +  "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.12  
    1.13 -lemma prod_rel_apply [simp]:
    1.14 -  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.15 -  by (simp add: prod_rel_def)
    1.16 +lemma rel_prod_apply [simp]:
    1.17 +  "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.18 +  by (simp add: rel_prod_def)
    1.19  
    1.20  bnf "'a \<times> 'b"
    1.21    map: map_prod
    1.22    sets: fsts snds
    1.23    bd: natLeq
    1.24 -  rel: prod_rel
    1.25 +  rel: rel_prod
    1.26  proof (unfold prod_set_defs)
    1.27    show "map_prod id id = id" by (rule map_prod.id)
    1.28  next
    1.29 @@ -149,13 +149,13 @@
    1.30      by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
    1.31  next
    1.32    fix R1 R2 S1 S2
    1.33 -  show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
    1.34 +  show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> rel_prod (R1 OO S1) (R2 OO S2)" by auto
    1.35  next
    1.36    fix R S
    1.37 -  show "prod_rel R S =
    1.38 +  show "rel_prod R S =
    1.39          (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
    1.40          Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
    1.41 -  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    1.42 +  unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    1.43    by auto
    1.44  qed
    1.45