src/HOL/Codatatype/Basic_BNFs.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 49312 c874ff5658dc
child 49434 433dc7e028c8
permissions -rw-r--r--
tuned simpset
     1 (*  Title:      HOL/Codatatype/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 bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
    28 apply auto
    29 apply (rule natLeq_card_order)
    30 apply (rule natLeq_cinfinite)
    31 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    32 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)
    33 apply (rule ordLeq_transitive)
    34 apply (rule ordLeq_cexp1[of natLeq])
    35 apply (rule Cinfinite_Cnotzero)
    36 apply (rule conjI)
    37 apply (rule natLeq_cinfinite)
    38 apply (rule natLeq_Card_order)
    39 apply (rule card_of_Card_order)
    40 apply (rule cexp_mono1)
    41 apply (rule ordLeq_csum1)
    42 apply (rule card_of_Card_order)
    43 apply (rule disjI2)
    44 apply (rule cone_ordLeq_cexp)
    45 apply (rule ordLeq_transitive)
    46 apply (rule cone_ordLeq_ctwo)
    47 apply (rule ordLeq_csum2)
    48 apply (rule Card_order_ctwo)
    49 apply (rule natLeq_Card_order)
    50 done
    51 
    52 lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>"
    53 unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto
    54 
    55 bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
    56 apply (auto simp add: wpull_id)
    57 apply (rule card_order_csum)
    58 apply (rule natLeq_card_order)
    59 apply (rule card_of_card_order_on)
    60 apply (rule cinfinite_csum)
    61 apply (rule disjI1)
    62 apply (rule natLeq_cinfinite)
    63 apply (rule ordLess_imp_ordLeq)
    64 apply (rule ordLess_ordLeq_trans)
    65 apply (rule ordLess_ctwo_cexp)
    66 apply (rule card_of_Card_order)
    67 apply (rule cexp_mono2'')
    68 apply (rule ordLeq_csum2)
    69 apply (rule card_of_Card_order)
    70 apply (rule ctwo_Cnotzero)
    71 by (rule card_of_Card_order)
    72 
    73 lemma DEADID_pred[simp]: "DEADID_pred = (op =)"
    74 unfolding DEADID_pred_def DEADID.rel_Id by simp
    75 
    76 ML {*
    77 signature BASIC_BNFS =
    78 sig
    79   val ID_bnf: BNF_Def.BNF
    80   val ID_rel_def: thm
    81   val ID_pred_def: thm
    82 
    83   val DEADID_bnf: BNF_Def.BNF
    84 end;
    85 
    86 structure Basic_BNFs : BASIC_BNFS =
    87 struct
    88 
    89 val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
    90 val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
    91 
    92 val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
    93 val ID_rel_def = rel_def RS sym;
    94 val ID_pred_def = Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym;
    95 
    96 end;
    97 *}
    98 
    99 definition sum_setl :: "'a + 'b \<Rightarrow> 'a set" where
   100 "sum_setl x = (case x of Inl z => {z} | _ => {})"
   101 
   102 definition sum_setr :: "'a + 'b \<Rightarrow> 'b set" where
   103 "sum_setr x = (case x of Inr z => {z} | _ => {})"
   104 
   105 lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def]
   106 
   107 bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
   108 proof -
   109   show "sum_map id id = id" by (rule sum_map.id)
   110 next
   111   fix f1 f2 g1 g2
   112   show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
   113     by (rule sum_map.comp[symmetric])
   114 next
   115   fix x f1 f2 g1 g2
   116   assume a1: "\<And>z. z \<in> sum_setl x \<Longrightarrow> f1 z = g1 z" and
   117          a2: "\<And>z. z \<in> sum_setr x \<Longrightarrow> f2 z = g2 z"
   118   thus "sum_map f1 f2 x = sum_map g1 g2 x"
   119   proof (cases x)
   120     case Inl thus ?thesis using a1 by (clarsimp simp: sum_setl_def)
   121   next
   122     case Inr thus ?thesis using a2 by (clarsimp simp: sum_setr_def)
   123   qed
   124 next
   125   fix f1 f2
   126   show "sum_setl o sum_map f1 f2 = image f1 o sum_setl"
   127     by (rule ext, unfold o_apply) (simp add: sum_setl_def split: sum.split)
   128 next
   129   fix f1 f2
   130   show "sum_setr o sum_map f1 f2 = image f2 o sum_setr"
   131     by (rule ext, unfold o_apply) (simp add: sum_setr_def split: sum.split)
   132 next
   133   show "card_order natLeq" by (rule natLeq_card_order)
   134 next
   135   show "cinfinite natLeq" by (rule natLeq_cinfinite)
   136 next
   137   fix x
   138   show "|sum_setl x| \<le>o natLeq"
   139     apply (rule ordLess_imp_ordLeq)
   140     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
   141     by (simp add: sum_setl_def split: sum.split)
   142 next
   143   fix x
   144   show "|sum_setr x| \<le>o natLeq"
   145     apply (rule ordLess_imp_ordLeq)
   146     apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
   147     by (simp add: sum_setr_def split: sum.split)
   148 next
   149   fix A1 :: "'a set" and A2 :: "'b set"
   150   have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and>
   151     (case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R")
   152   proof safe
   153     fix x :: "'a + 'b"
   154     assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2"
   155     hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+
   156     thus "x \<in> A1 <+> A2" by blast
   157   qed (auto split: sum.split)
   158   show "|{x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2}| \<le>o
   159     (( |A1| +c |A2| ) +c ctwo) ^c natLeq"
   160     apply (rule ordIso_ordLeq_trans)
   161     apply (rule card_of_ordIso_subst)
   162     apply (unfold sum_set_defs)
   163     apply (rule in_alt)
   164     apply (rule ordIso_ordLeq_trans)
   165     apply (rule Plus_csum)
   166     apply (rule ordLeq_transitive)
   167     apply (rule ordLeq_csum1)
   168     apply (rule Card_order_csum)
   169     apply (rule ordLeq_cexp1)
   170     apply (rule conjI)
   171     using Field_natLeq UNIV_not_empty czeroE apply fast
   172     apply (rule natLeq_Card_order)
   173     by (rule Card_order_csum)
   174 next
   175   fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
   176   assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
   177   hence
   178     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"
   179     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"
   180     unfolding wpull_def by blast+
   181   show "wpull {x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2}
   182   {x. sum_setl x \<subseteq> B11 \<and> sum_setr x \<subseteq> B12} {x. sum_setl x \<subseteq> B21 \<and> sum_setr x \<subseteq> B22}
   183   (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
   184     (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
   185   proof (unfold wpull_def)
   186     { fix B1 B2
   187       assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
   188       have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
   189       proof (cases B1)
   190         case (Inl b1)
   191         { fix b2 assume "B2 = Inr b2"
   192           with Inl *(3) have False by simp
   193         } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
   194         with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
   195         by (simp add: sum_setl_def)+
   196         with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
   197         with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
   198         by (simp add: sum_set_defs)+
   199         thus ?thesis by blast
   200       next
   201         case (Inr b1)
   202         { fix b2 assume "B2 = Inl b2"
   203           with Inr *(3) have False by simp
   204         } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
   205         with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
   206         by (simp add: sum_set_defs)+
   207         with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
   208         with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
   209         by (simp add: sum_set_defs)+
   210         thus ?thesis by blast
   211       qed
   212     }
   213     thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
   214       (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
   215   qed
   216 qed (auto simp: sum_set_defs)
   217 
   218 lemma sum_pred[simp]:
   219   "sum_pred \<phi> \<psi> x y =
   220     (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
   221              | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
   222 unfolding sum_setl_def sum_setr_def sum_pred_def sum_rel_def Gr_def relcomp_unfold converse_unfold
   223 by (fastforce split: sum.splits)+
   224 
   225 lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq"
   226   apply (rule ordLeq_transitive)
   227   apply (rule ordLeq_cprod2)
   228   apply (rule ctwo_Cnotzero)
   229   apply (auto simp: Field_card_of intro: card_of_card_order_on)
   230   apply (rule cprod_mono2)
   231   apply (rule ordLess_imp_ordLeq)
   232   apply (unfold finite_iff_ordLess_natLeq[symmetric])
   233   by simp
   234 
   235 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
   236 "fsts x = {fst x}"
   237 
   238 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
   239 "snds x = {snd x}"
   240 
   241 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
   242 
   243 bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
   244 proof (unfold prod_set_defs)
   245   show "map_pair id id = id" by (rule map_pair.id)
   246 next
   247   fix f1 f2 g1 g2
   248   show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
   249     by (rule map_pair.comp[symmetric])
   250 next
   251   fix x f1 f2 g1 g2
   252   assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
   253   thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
   254 next
   255   fix f1 f2
   256   show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
   257     by (rule ext, unfold o_apply) simp
   258 next
   259   fix f1 f2
   260   show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
   261     by (rule ext, unfold o_apply) simp
   262 next
   263   show "card_order (ctwo *c natLeq)"
   264     apply (rule card_order_cprod)
   265     apply (rule ctwo_card_order)
   266     by (rule natLeq_card_order)
   267 next
   268   show "cinfinite (ctwo *c natLeq)"
   269     apply (rule cinfinite_cprod2)
   270     apply (rule ctwo_Cnotzero)
   271     apply (rule conjI[OF _ natLeq_Card_order])
   272     by (rule natLeq_cinfinite)
   273 next
   274   fix x
   275   show "|{fst x}| \<le>o ctwo *c natLeq"
   276     by (rule singleton_ordLeq_ctwo_natLeq)
   277 next
   278   fix x
   279   show "|{snd x}| \<le>o ctwo *c natLeq"
   280     by (rule singleton_ordLeq_ctwo_natLeq)
   281 next
   282   fix A1 :: "'a set" and A2 :: "'b set"
   283   have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto
   284   show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o
   285     ( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)"
   286     apply (rule ordIso_ordLeq_trans)
   287     apply (rule card_of_ordIso_subst)
   288     apply (rule in_alt)
   289     apply (rule ordIso_ordLeq_trans)
   290     apply (rule Times_cprod)
   291     apply (rule ordLeq_transitive)
   292     apply (rule cprod_csum_cexp)
   293     apply (rule cexp_mono)
   294     apply (rule ordLeq_csum1)
   295     apply (rule Card_order_csum)
   296     apply (rule ordLeq_cprod1)
   297     apply (rule Card_order_ctwo)
   298     apply (rule Cinfinite_Cnotzero)
   299     apply (rule conjI[OF _ natLeq_Card_order])
   300     apply (rule natLeq_cinfinite)
   301     apply (rule disjI2)
   302     apply (rule cone_ordLeq_cexp)
   303     apply (rule ordLeq_transitive)
   304     apply (rule cone_ordLeq_ctwo)
   305     apply (rule ordLeq_csum2)
   306     apply (rule Card_order_ctwo)
   307     apply (rule notE)
   308     apply (rule ctwo_not_czero)
   309     apply assumption
   310     by (rule Card_order_ctwo)
   311 next
   312   fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
   313   assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
   314   thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
   315     {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
   316    (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
   317     unfolding wpull_def by simp fast
   318 qed simp+
   319 
   320 lemma prod_pred[simp]:
   321 "prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> (\<phi> a1 a2 \<and> \<psi> b1 b2))"
   322 unfolding prod_set_defs prod_pred_def prod_rel_def Gr_def relcomp_unfold converse_unfold by auto
   323 (* TODO: pred characterization for each basic BNF *)
   324 
   325 (* Categorical version of pullback: *)
   326 lemma wpull_cat:
   327 assumes p: "wpull A B1 B2 f1 f2 p1 p2"
   328 and c: "f1 o q1 = f2 o q2"
   329 and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
   330 obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
   331 proof-
   332   have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
   333   proof safe
   334     fix d
   335     have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
   336     moreover
   337     have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
   338     ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
   339       using p unfolding wpull_def by auto
   340   qed
   341   then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
   342   thus ?thesis using that by fastforce
   343 qed
   344 
   345 lemma card_of_bounded_range:
   346   "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
   347 proof -
   348   let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None"
   349   have "inj_on ?f ?LHS" unfolding inj_on_def
   350   proof (unfold fun_eq_iff, safe)
   351     fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
   352     assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
   353     hence "f x \<in> B" "g x \<in> B" by auto
   354     with eq have "Some (f x) = Some (g x)" by metis
   355     thus "f x = g x" by simp
   356   qed
   357   moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
   358   ultimately show ?thesis using card_of_ordLeq by fast
   359 qed
   360 
   361 bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
   362   ["%c x::'b::type. c::'a::type"]
   363 proof
   364   fix f show "id \<circ> f = id f" by simp
   365 next
   366   fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
   367   unfolding comp_def[abs_def] ..
   368 next
   369   fix x f g
   370   assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
   371   thus "f \<circ> x = g \<circ> x" by auto
   372 next
   373   fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
   374   unfolding image_def comp_def[abs_def] by auto
   375 next
   376   show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
   377   apply (rule card_order_csum)
   378   apply (rule natLeq_card_order)
   379   by (rule card_of_card_order_on)
   380 (*  *)
   381   show "cinfinite (natLeq +c ?U)"
   382     apply (rule cinfinite_csum)
   383     apply (rule disjI1)
   384     by (rule natLeq_cinfinite)
   385 next
   386   fix f :: "'d => 'a"
   387   have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
   388   also have "?U \<le>o natLeq +c ?U"  by (rule ordLeq_csum2) (rule card_of_Card_order)
   389   finally show "|range f| \<le>o natLeq +c ?U" .
   390 next
   391   fix B :: "'a set"
   392   have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range)
   393   also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|"
   394     unfolding cexp_def Field_card_of by (rule card_of_refl)
   395   also have "|B| ^c |UNIV :: 'd set| \<le>o
   396              ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )"
   397     apply (rule cexp_mono)
   398      apply (rule ordLeq_csum1) apply (rule card_of_Card_order)
   399      apply (rule ordLeq_csum2) apply (rule card_of_Card_order)
   400      apply (rule disjI2) apply (rule cone_ordLeq_cexp)
   401       apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2)
   402       apply (rule Card_order_ctwo)
   403      apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast
   404      apply (rule card_of_Card_order)
   405   done
   406   finally
   407   show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o
   408         ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" .
   409 next
   410   fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
   411   show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
   412     (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
   413   unfolding wpull_def
   414   proof safe
   415     fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
   416     and c: "f1 \<circ> g1 = f2 \<circ> g2"
   417     show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
   418     using wpull_cat[OF p c r] by simp metis
   419   qed
   420 qed auto
   421 
   422 lemma fun_pred[simp]: "fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
   423 unfolding fun_rel_def fun_pred_def Gr_def relcomp_unfold converse_unfold
   424 by (auto intro!: exI dest!: in_mono)
   425 
   426 end