Quelle BNF_Composition.thy

Sprache: Isabelle

(*  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 ==> |{}|
  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| "∧i. i ∈ I ==> |A i|
  shows "|∪i∈I. A i|
  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| and
    gset_bd: "∧x. |gset x|
  shows "|∪(fset ` gset x)|
proof (cases "fbd )
  case True
  then have "|fset x| for x using fset_bd ordLess_transitive by blast
  then have "|∪(fset ` gset x)| using regularCard_UNION_bound[OF gbd gset_bd] by blast
  then have "|∪ (fset ` gset x)|
    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| for x using gset_bd ordLess_ordLeq_trans by blast
  then have "|∪(fset ` gset x)| 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))| ==> |(Union ∘ collect X) x|
  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)^-1^-1 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)^-1^-1 OO Grp A g = (Grp B f)^-1^-1 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| ==> |(S ∘ Rep) x|
  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^-1^-1 OO S) = (vimage2p Rep f R)^-1^-1 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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-04-26) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.