# Theory BNF_Composition

theory BNF_Composition
imports BNF_Def
```(*  Title:      HOL/BNF_Composition.thy
Author:     Dmitriy Traytel, TU Muenchen
Author:     Jasmin Blanchette, TU Muenchen

Composition of bounded natural functors.
*)

section ‹Composition of Bounded Natural Functors›

theory BNF_Composition
imports BNF_Def
keywords
"copy_bnf" :: thy_decl and
"lift_bnf" :: thy_goal
begin

lemma ssubst_mem: "⟦t = s; s ∈ X⟧ ⟹ t ∈ X"
by simp

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

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

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

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)
apply (rule ordLess_imp_ordLeq[OF 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"
ML_file "Tools/BNF/bnf_lift.ML"

hide_fact