Theory BNF_Composition
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 "|⋃i∈I. 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