src/HOL/BNF/Basic_BNFs.thy
author blanchet
Tue Apr 30 13:34:31 2013 +0200 (2013-04-30)
changeset 51836 4d6dcd51dd52
parent 51782 84e7225f5ab6
child 51893 596baae88a88
permissions -rw-r--r--
renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
     1 (*  Title:      HOL/BNF/Basic_BNFs.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Andrei Popescu, TU Muenchen
     4     Author:     Jasmin Blanchette, TU Muenchen
     5     Copyright   2012
     6 
     7 Registration of basic types as bounded natural functors.
     8 *)
     9 
    10 header {* Registration of Basic Types as Bounded Natural Functors *}
    11 
    12 theory Basic_BNFs
    13 imports BNF_Def
    14 begin
    15 
    16 lemma wpull_id: "wpull UNIV B1 B2 id id id id"
    17 unfolding wpull_def by simp
    18 
    19 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
    20 
    21 lemma ctwo_card_order: "card_order ctwo"
    22 using Card_order_ctwo by (unfold ctwo_def Field_card_of)
    23 
    24 lemma natLeq_cinfinite: "cinfinite natLeq"
    25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
    26 
    27 lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
    28   unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
    29 
    30 bnf ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
    31   "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
    32 apply (auto simp: Gr_def fun_eq_iff natLeq_card_order natLeq_cinfinite)
    33 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    34 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    35 apply (rule ordLeq_transitive)
    36 apply (rule ordLeq_cexp1[of natLeq])
    37 apply (rule Cinfinite_Cnotzero)
    38 apply (rule conjI)
    39 apply (rule natLeq_cinfinite)
    40 apply (rule natLeq_Card_order)
    41 apply (rule card_of_Card_order)
    42 apply (rule cexp_mono1)
    43 apply (rule ordLeq_csum1)
    44 apply (rule card_of_Card_order)
    45 apply (rule natLeq_Card_order)
    46 done
    47 
    48 bnf DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
    49   "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
    50 apply (auto simp add: wpull_Gr_def Gr_def
    51   card_order_csum natLeq_card_order card_of_card_order_on
    52   cinfinite_csum natLeq_cinfinite)
    53 apply (rule ordLess_imp_ordLeq)
    54 apply (rule ordLess_ordLeq_trans)
    55 apply (rule ordLess_ctwo_cexp)
    56 apply (rule card_of_Card_order)
    57 apply (rule cexp_mono2'')
    58 apply (rule ordLeq_csum2)
    59 apply (rule card_of_Card_order)
    60 apply (rule ctwo_Cnotzero)
    61 apply (rule card_of_Card_order)
    62 done
    63 
    64 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    65 "setl x = (case x of Inl z => {z} | _ => {})"
    66 
    67 definition setr :: "'a + 'b \<Rightarrow> 'b set" where
    68 "setr x = (case x of Inr z => {z} | _ => {})"
    69 
    70 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
    71 
    72 definition sum_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
    73 "sum_rel \<phi> \<psi> x y =
    74  (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
    75           | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
    76 
    77 bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
    78 proof -
    79   show "sum_map id id = id" by (rule sum_map.id)
    80 next
    81   fix f1 f2 g1 g2
    82   show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
    83     by (rule sum_map.comp[symmetric])
    84 next
    85   fix x f1 f2 g1 g2
    86   assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
    87          a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
    88   thus "sum_map f1 f2 x = sum_map g1 g2 x"
    89   proof (cases x)
    90     case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
    91   next
    92     case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
    93   qed
    94 next
    95   fix f1 f2
    96   show "setl o sum_map f1 f2 = image f1 o setl"
    97     by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
    98 next
    99   fix f1 f2
   100   show "setr o sum_map f1 f2 = image f2 o setr"
   101     by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
   102 next
   103   show "card_order natLeq" by (rule natLeq_card_order)
   104 next
   105   show "cinfinite natLeq" by (rule natLeq_cinfinite)
   106 next
   107   fix x
   108   show "|setl x| \<le>o natLeq"
   109     apply (rule ordLess_imp_ordLeq)
   110     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
   111     by (simp add: setl_def split: sum.split)
   112 next
   113   fix x
   114   show "|setr x| \<le>o natLeq"
   115     apply (rule ordLess_imp_ordLeq)
   116     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
   117     by (simp add: setr_def split: sum.split)
   118 next
   119   fix A1 :: "'a set" and A2 :: "'b set"
   120   have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and>
   121     (case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R")
   122   proof safe
   123     fix x :: "'a + 'b"
   124     assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2"
   125     hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+
   126     thus "x \<in> A1 <+> A2" by blast
   127   qed (auto split: sum.split)
   128   show "|{x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}| \<le>o
   129     (( |A1| +c |A2| ) +c ctwo) ^c natLeq"
   130     apply (rule ordIso_ordLeq_trans)
   131     apply (rule card_of_ordIso_subst)
   132     apply (unfold sum_set_defs)
   133     apply (rule in_alt)
   134     apply (rule ordIso_ordLeq_trans)
   135     apply (rule Plus_csum)
   136     apply (rule ordLeq_transitive)
   137     apply (rule ordLeq_csum1)
   138     apply (rule Card_order_csum)
   139     apply (rule ordLeq_cexp1)
   140     apply (rule conjI)
   141     using Field_natLeq UNIV_not_empty czeroE apply fast
   142     apply (rule natLeq_Card_order)
   143     by (rule Card_order_csum)
   144 next
   145   fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
   146   assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
   147   hence
   148     pull1: "\<And>b1 b2. \<lbrakk>b1 \<in> B11; b2 \<in> B21; f11 b1 = f21 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A1. p11 a = b1 \<and> p21 a = b2"
   149     and pull2: "\<And>b1 b2. \<lbrakk>b1 \<in> B12; b2 \<in> B22; f12 b1 = f22 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A2. p12 a = b1 \<and> p22 a = b2"
   150     unfolding wpull_def by blast+
   151   show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}
   152   {x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22}
   153   (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
   154     (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
   155   proof (unfold wpull_def)
   156     { fix B1 B2
   157       assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
   158       have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
   159       proof (cases B1)
   160         case (Inl b1)
   161         { fix b2 assume "B2 = Inr b2"
   162           with Inl *(3) have False by simp
   163         } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
   164         with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
   165         by (simp add: setl_def)+
   166         with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
   167         with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
   168         by (simp add: sum_set_defs)+
   169         thus ?thesis by blast
   170       next
   171         case (Inr b1)
   172         { fix b2 assume "B2 = Inl b2"
   173           with Inr *(3) have False by simp
   174         } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
   175         with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
   176         by (simp add: sum_set_defs)+
   177         with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
   178         with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
   179         by (simp add: sum_set_defs)+
   180         thus ?thesis by blast
   181       qed
   182     }
   183     thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
   184       (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
   185   qed
   186 next
   187   fix R S
   188   show "{p. sum_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
   189         (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O
   190         Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)"
   191   unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold
   192   by (fastforce split: sum.splits)
   193 qed (auto simp: sum_set_defs)
   194 
   195 lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq"
   196   apply (rule ordLeq_transitive)
   197   apply (rule ordLeq_cprod2)
   198   apply (rule ctwo_Cnotzero)
   199   apply (auto simp: Field_card_of intro: card_of_card_order_on)
   200   apply (rule cprod_mono2)
   201   apply (rule ordLess_imp_ordLeq)
   202   apply (unfold finite_iff_ordLess_natLeq[symmetric])
   203   by simp
   204 
   205 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
   206 "fsts x = {fst x}"
   207 
   208 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
   209 "snds x = {snd x}"
   210 
   211 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
   212 
   213 definition prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
   214 "prod_rel \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
   215 
   216 bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
   217 proof (unfold prod_set_defs)
   218   show "map_pair id id = id" by (rule map_pair.id)
   219 next
   220   fix f1 f2 g1 g2
   221   show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
   222     by (rule map_pair.comp[symmetric])
   223 next
   224   fix x f1 f2 g1 g2
   225   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
   226   thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
   227 next
   228   fix f1 f2
   229   show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
   230     by (rule ext, unfold o_apply) simp
   231 next
   232   fix f1 f2
   233   show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
   234     by (rule ext, unfold o_apply) simp
   235 next
   236   show "card_order (ctwo *c natLeq)"
   237     apply (rule card_order_cprod)
   238     apply (rule ctwo_card_order)
   239     by (rule natLeq_card_order)
   240 next
   241   show "cinfinite (ctwo *c natLeq)"
   242     apply (rule cinfinite_cprod2)
   243     apply (rule ctwo_Cnotzero)
   244     apply (rule conjI[OF _ natLeq_Card_order])
   245     by (rule natLeq_cinfinite)
   246 next
   247   fix x
   248   show "|{fst x}| \<le>o ctwo *c natLeq"
   249     by (rule singleton_ordLeq_ctwo_natLeq)
   250 next
   251   fix x
   252   show "|{snd x}| \<le>o ctwo *c natLeq"
   253     by (rule singleton_ordLeq_ctwo_natLeq)
   254 next
   255   fix A1 :: "'a set" and A2 :: "'b set"
   256   have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto
   257   show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o
   258     ( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)"
   259     apply (rule ordIso_ordLeq_trans)
   260     apply (rule card_of_ordIso_subst)
   261     apply (rule in_alt)
   262     apply (rule ordIso_ordLeq_trans)
   263     apply (rule Times_cprod)
   264     apply (rule ordLeq_transitive)
   265     apply (rule cprod_csum_cexp)
   266     apply (rule cexp_mono)
   267     apply (rule ordLeq_csum1)
   268     apply (rule Card_order_csum)
   269     apply (rule ordLeq_cprod1)
   270     apply (rule Card_order_ctwo)
   271     apply (rule Cinfinite_Cnotzero)
   272     apply (rule conjI[OF _ natLeq_Card_order])
   273     apply (rule natLeq_cinfinite)
   274     apply (rule notE)
   275     apply (rule ctwo_not_czero)
   276     apply assumption
   277     by (rule Card_order_ctwo)
   278 next
   279   fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
   280   assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
   281   thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
   282     {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
   283    (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
   284     unfolding wpull_def by simp fast
   285 next
   286   fix R S
   287   show "{p. prod_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} =
   288         (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O
   289         Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)"
   290   unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold
   291   by auto
   292 qed simp+
   293 
   294 (* Categorical version of pullback: *)
   295 lemma wpull_cat:
   296 assumes p: "wpull A B1 B2 f1 f2 p1 p2"
   297 and c: "f1 o q1 = f2 o q2"
   298 and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
   299 obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
   300 proof-
   301   have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
   302   proof safe
   303     fix d
   304     have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
   305     moreover
   306     have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
   307     ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
   308       using p unfolding wpull_def by auto
   309   qed
   310   then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
   311   thus ?thesis using that by fastforce
   312 qed
   313 
   314 lemma card_of_bounded_range:
   315   "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
   316 proof -
   317   let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None"
   318   have "inj_on ?f ?LHS" unfolding inj_on_def
   319   proof (unfold fun_eq_iff, safe)
   320     fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
   321     assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
   322     hence "f x \<in> B" "g x \<in> B" by auto
   323     with eq have "Some (f x) = Some (g x)" by metis
   324     thus "f x = g x" by simp
   325   qed
   326   moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
   327   ultimately show ?thesis using card_of_ordLeq by fast
   328 qed
   329 
   330 bnf "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
   331   "fun_rel op ="
   332 proof
   333   fix f show "id \<circ> f = id f" by simp
   334 next
   335   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
   336   unfolding comp_def[abs_def] ..
   337 next
   338   fix x f g
   339   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
   340   thus "f \<circ> x = g \<circ> x" by auto
   341 next
   342   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
   343   unfolding image_def comp_def[abs_def] by auto
   344 next
   345   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
   346   apply (rule card_order_csum)
   347   apply (rule natLeq_card_order)
   348   by (rule card_of_card_order_on)
   349 (*  *)
   350   show "cinfinite (natLeq +c ?U)"
   351     apply (rule cinfinite_csum)
   352     apply (rule disjI1)
   353     by (rule natLeq_cinfinite)
   354 next
   355   fix f :: "'d => 'a"
   356   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
   357   also have "?U \<le>o natLeq +c ?U"  by (rule ordLeq_csum2) (rule card_of_Card_order)
   358   finally show "|range f| \<le>o natLeq +c ?U" .
   359 next
   360   fix B :: "'a set"
   361   have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range)
   362   also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|"
   363     unfolding cexp_def Field_card_of by (rule card_of_refl)
   364   also have "|B| ^c |UNIV :: 'd set| \<le>o
   365              ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )"
   366     apply (rule cexp_mono)
   367      apply (rule ordLeq_csum1) apply (rule card_of_Card_order)
   368      apply (rule ordLeq_csum2) apply (rule card_of_Card_order)
   369      apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast
   370      apply (rule card_of_Card_order)
   371   done
   372   finally
   373   show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o
   374         ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" .
   375 next
   376   fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
   377   show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
   378     (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
   379   unfolding wpull_def
   380   proof safe
   381     fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
   382     and c: "f1 \<circ> g1 = f2 \<circ> g2"
   383     show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
   384     using wpull_cat[OF p c r] by simp metis
   385   qed
   386 next
   387   fix R
   388   show "{p. fun_rel op = (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
   389         (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
   390   unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold
   391   by force
   392 qed auto
   393 
   394 end