Theory HOL.BNF_Composition

(*  Title:      HOL/BNF_Composition.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Jan van Brügge, TU Muenchen
    Copyright   2012, 2013, 2014, 2022

Composition of bounded natural functors.
*)

section ‹Composition of Bounded Natural Functors›

theory BNF_Composition
imports BNF_Def
begin

lemma ssubst_mem: "t = s; s  X  t  X"
  by simp

lemma empty_natural: "(λ_. {})  f = image g  (λ_. {})"
  by (rule ext) simp

lemma Cinfinite_gt_empty: "Cinfinite r  |{}| <o r"
  by (simp add: cinfinite_def finite_ordLess_infinite card_of_ordIso_finite Field_card_of card_of_well_order_on emptyI card_order_on_well_order_on)

lemma Union_natural: "Union  image (image f) = image f  Union"
  by (rule ext) (auto simp only: comp_apply)

lemma in_Union_o_assoc: "x  (Union  gset  gmap) A  x  (Union  (gset  gmap)) A"
  by (unfold comp_assoc)

lemma regularCard_UNION_bound:
  assumes "Cinfinite r" "regularCard r" and "|I| <o r" "i. i  I  |A i| <o r"
  shows "|iI. A i| <o r"
  using assms cinfinite_def regularCard_stable stable_UNION by blast

lemma comp_single_set_bd_strict:
  assumes fbd: "Cinfinite fbd" "regularCard fbd" and
    gbd: "Cinfinite gbd" "regularCard gbd" and
    fset_bd: "x. |fset x| <o fbd" and
    gset_bd: "x. |gset x| <o gbd"
  shows "|(fset ` gset x)| <o gbd *c fbd"
proof (cases "fbd <o gbd")
  case True
  then have "|fset x| <o gbd" for x using fset_bd ordLess_transitive by blast
  then have "|(fset ` gset x)| <o gbd" using regularCard_UNION_bound[OF gbd gset_bd] by blast
  then have "| (fset ` gset x)| <o fbd *c gbd"
    using ordLess_ordLeq_trans ordLeq_cprod2 gbd(1) fbd(1) cinfinite_not_czero by blast
  then show ?thesis using ordLess_ordIso_trans cprod_com by blast
next
  case False
  have "Well_order fbd" "Well_order gbd" using fbd(1) gbd(1) card_order_on_well_order_on by auto
  then have "gbd ≤o fbd" using not_ordLess_iff_ordLeq False by blast
  then have "|gset x| <o fbd" for x using gset_bd ordLess_ordLeq_trans by blast
  then have "|(fset ` gset x)| <o fbd" using regularCard_UNION_bound[OF fbd] fset_bd by blast
  then show ?thesis using ordLess_ordLeq_trans ordLeq_cprod2 gbd(1) fbd(1) cinfinite_not_czero by blast
qed

lemma comp_single_set_bd:
  assumes fbd_Card_order: "Card_order fbd" and
    fset_bd: "x. |fset x| ≤o fbd" and
    gset_bd: "x. |gset x| ≤o gbd"
  shows "|(fset ` gset x)| ≤o gbd *c fbd"
  apply simp
  apply (rule ordLeq_transitive)
  apply (rule card_of_UNION_Sigma)
  apply (subst SIGMA_CSUM)
  apply (rule ordLeq_transitive)
  apply (rule card_of_Csum_Times')
  apply (rule fbd_Card_order)
  apply (rule ballI)
  apply (rule fset_bd)
  apply (rule ordLeq_transitive)
  apply (rule cprod_mono1)
  apply (rule gset_bd)
  apply (rule ordIso_imp_ordLeq)
  apply (rule ordIso_refl)
  apply (rule Card_order_cprod)
  done

lemma csum_dup: "cinfinite r  Card_order r  p +c p' =o r +c r  p +c p' =o r"
  apply (erule ordIso_transitive)
  apply (frule csum_absorb2')
  apply (erule ordLeq_refl)
  by simp

lemma cprod_dup: "cinfinite r  Card_order r  p *c p' =o r *c r  p *c p' =o r"
  apply (erule ordIso_transitive)
  apply (rule cprod_infinite)
  by simp

lemma Union_image_insert: "(f ` insert a B) = f a  (f ` B)"
  by simp

lemma Union_image_empty: "A  (f ` {}) = A"
  by simp

lemma image_o_collect: "collect ((λf. image g  f) ` F) = image g  collect F"
  by (rule ext) (auto simp add: collect_def)

lemma conj_subset_def: "A  {x. P x  Q x} = (A  {x. P x}  A  {x. Q x})"
  by blast

lemma UN_image_subset: "(f ` g x)  X = (g x  {x. f x  X})"
  by blast

lemma comp_set_bd_Union_o_collect: "|(((λf. f x) ` X))| ≤o hbd  |(Union  collect X) x| ≤o hbd"
  by (unfold comp_apply collect_def) simp

lemma comp_set_bd_Union_o_collect_strict: "|(((λf. f x) ` X))| <o hbd  |(Union  collect X) x| <o hbd"
  by (unfold comp_apply collect_def) simp

lemma Collect_inj: "Collect P = Collect Q  P = Q"
  by blast

lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)¯¯ OO Grp (Collect (case_prod R)) snd = R"
  unfolding Grp_def fun_eq_iff relcompp.simps by auto

lemma OO_Grp_cong: "A = B  (Grp A f)¯¯ OO Grp A g = (Grp B f)¯¯ OO Grp B g"
  by (rule arg_cong)

lemma vimage2p_relcompp_mono: "R OO S  T 
  vimage2p f g R OO vimage2p g h S  vimage2p f h T"
  unfolding vimage2p_def by auto

lemma type_copy_map_cong0: "M (g x) = N (h x)  (f  M  g) x = (f  N  h) x"
  by auto

lemma type_copy_set_bd: "(y. |S y| <o bd)  |(S  Rep) x| <o bd"
  by auto

lemma vimage2p_cong: "R = S  vimage2p f g R = vimage2p f g S"
  by simp

lemma Ball_comp_iff: "(λx. Ball (A x) f)  g = (λx. Ball ((A  g) x) f)"
  unfolding o_def by auto

lemma conj_comp_iff: "(λx. P x  Q x)  g = (λx. (P  g) x  (Q  g) x)"
  unfolding o_def by auto

context
  fixes Rep Abs
  assumes type_copy: "type_definition Rep Abs UNIV"
begin

lemma type_copy_map_id0: "M = id  Abs  M  Rep = id"
  using type_definition.Rep_inverse[OF type_copy] by auto

lemma type_copy_map_comp0: "M = M1  M2  f  M  g = (f  M1  Rep)  (Abs  M2  g)"
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto

lemma type_copy_set_map0: "S  M = image f  S'  (S  Rep)  (Abs  M  g) = image f  (S'  g)"
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)

lemma type_copy_wit: "x  (S  Rep) (Abs y)  x  S y"
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto

lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
    Grp (Collect (λx. P (f x))) (Abs  h  f)"
  unfolding vimage2p_def Grp_def fun_eq_iff
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   type_definition.Rep_inverse[OF type_copy] dest: sym)

lemma type_copy_vimage2p_Grp_Abs:
  "h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (λx. P (g x))) (Rep  h  g)"
  unfolding vimage2p_def Grp_def fun_eq_iff
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   type_definition.Rep_inverse[OF type_copy] dest: sym)

lemma type_copy_ex_RepI: "(b. F b) = (b. F (Rep b))"
proof safe
  fix b assume "F b"
  show "b'. F (Rep b')"
  proof (rule exI)
    from F b show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
  qed
qed blast

lemma vimage2p_relcompp_converse:
  "vimage2p f g (R¯¯ OO S) = (vimage2p Rep f R)¯¯ OO vimage2p Rep g S"
  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
  by (auto simp: type_copy_ex_RepI)

end

bnf DEADID: 'a
  map: "id :: 'a  'a"
  bd: natLeq
  rel: "(=) :: 'a  'a  bool"
  by (auto simp add: natLeq_card_order natLeq_cinfinite regularCard_natLeq)

definition id_bnf :: "'a  'a" where
  "id_bnf  (λx. x)"

lemma id_bnf_apply: "id_bnf x = x"
  unfolding id_bnf_def by simp

bnf ID: 'a
  map: "id_bnf :: ('a  'b)  'a  'b"
  sets: "λx. {x}"
  bd: natLeq
  rel: "id_bnf :: ('a  'b  bool)  'a  'b  bool"
  pred: "id_bnf :: ('a  bool)  'a  bool"
  unfolding id_bnf_def
  apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite regularCard_natLeq)
  apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
  apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
  done

lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
  unfolding id_bnf_def by unfold_locales auto

ML_file ‹Tools/BNF/bnf_comp_tactics.ML›
ML_file ‹Tools/BNF/bnf_comp.ML›

hide_fact
  DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0
  DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer
  DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq
  DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer
  ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id
  ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep
  ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer

end