src/HOL/BNF_Composition.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62324 ae44f16dcea5
child 62777 596baa1a3251
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/BNF_Composition.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012, 2013, 2014
     5 
     6 Composition of bounded natural functors.
     7 *)
     8 
     9 section \<open>Composition of Bounded Natural Functors\<close>
    10 
    11 theory BNF_Composition
    12 imports BNF_Def
    13 keywords
    14   "copy_bnf" :: thy_decl and
    15   "lift_bnf" :: thy_goal
    16 begin
    17 
    18 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X"
    19   by simp
    20 
    21 lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
    22   by (rule ext) simp
    23 
    24 lemma Union_natural: "Union o image (image f) = image f o Union"
    25   by (rule ext) (auto simp only: comp_apply)
    26 
    27 lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    28   by (unfold comp_assoc)
    29 
    30 lemma comp_single_set_bd:
    31   assumes fbd_Card_order: "Card_order fbd" and
    32     fset_bd: "\<And>x. |fset x| \<le>o fbd" and
    33     gset_bd: "\<And>x. |gset x| \<le>o gbd"
    34   shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
    35   apply simp
    36   apply (rule ordLeq_transitive)
    37   apply (rule card_of_UNION_Sigma)
    38   apply (subst SIGMA_CSUM)
    39   apply (rule ordLeq_transitive)
    40   apply (rule card_of_Csum_Times')
    41   apply (rule fbd_Card_order)
    42   apply (rule ballI)
    43   apply (rule fset_bd)
    44   apply (rule ordLeq_transitive)
    45   apply (rule cprod_mono1)
    46   apply (rule gset_bd)
    47   apply (rule ordIso_imp_ordLeq)
    48   apply (rule ordIso_refl)
    49   apply (rule Card_order_cprod)
    50   done
    51 
    52 lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
    53   apply (erule ordIso_transitive)
    54   apply (frule csum_absorb2')
    55   apply (erule ordLeq_refl)
    56   by simp
    57 
    58 lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    59   apply (erule ordIso_transitive)
    60   apply (rule cprod_infinite)
    61   by simp
    62 
    63 lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
    64   by simp
    65 
    66 lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
    67   by simp
    68 
    69 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
    70   by (rule ext) (auto simp add: collect_def)
    71 
    72 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    73   by blast
    74 
    75 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    76   by blast
    77 
    78 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
    79   by (unfold comp_apply collect_def) simp
    80 
    81 lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
    82   by blast
    83 
    84 lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))"
    85 by auto
    86 
    87 lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R"
    88   unfolding Grp_def fun_eq_iff relcompp.simps by auto
    89 
    90 lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
    91   by (rule arg_cong)
    92 
    93 lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
    94   vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
    95   unfolding vimage2p_def by auto
    96 
    97 lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x"
    98   by auto
    99 
   100 lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
   101   by auto
   102 
   103 lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
   104   by simp
   105 
   106 lemma Ball_comp_iff: "(\<lambda>x. Ball (A x) f) o g = (\<lambda>x. Ball ((A o g) x) f)"
   107   unfolding o_def by auto
   108 
   109 lemma conj_comp_iff: "(\<lambda>x. P x \<and> Q x) o g = (\<lambda>x. (P o g) x \<and> (Q o g) x)"
   110   unfolding o_def by auto
   111 
   112 context
   113   fixes Rep Abs
   114   assumes type_copy: "type_definition Rep Abs UNIV"
   115 begin
   116 
   117 lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
   118   using type_definition.Rep_inverse[OF type_copy] by auto
   119 
   120 lemma type_copy_map_comp0: "M = M1 o M2 \<Longrightarrow> f o M o g = (f o M1 o Rep) o (Abs o M2 o g)"
   121   using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   122 
   123 lemma type_copy_set_map0: "S o M = image f o S' \<Longrightarrow> (S o Rep) o (Abs o M o g) = image f o (S' o g)"
   124   using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
   125 
   126 lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
   127   using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   128 
   129 lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
   130     Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
   131   unfolding vimage2p_def Grp_def fun_eq_iff
   132   by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   133    type_definition.Rep_inverse[OF type_copy] dest: sym)
   134 
   135 lemma type_copy_vimage2p_Grp_Abs:
   136   "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
   137   unfolding vimage2p_def Grp_def fun_eq_iff
   138   by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   139    type_definition.Rep_inverse[OF type_copy] dest: sym)
   140 
   141 lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
   142 proof safe
   143   fix b assume "F b"
   144   show "\<exists>b'. F (Rep b')"
   145   proof (rule exI)
   146     from \<open>F b\<close> show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
   147   qed
   148 qed blast
   149 
   150 lemma vimage2p_relcompp_converse:
   151   "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
   152   unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
   153   by (auto simp: type_copy_ex_RepI)
   154 
   155 end
   156 
   157 bnf DEADID: 'a
   158   map: "id :: 'a \<Rightarrow> 'a"
   159   bd: natLeq
   160   rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
   161   by (auto simp add: natLeq_card_order natLeq_cinfinite)
   162 
   163 definition id_bnf :: "'a \<Rightarrow> 'a" where
   164   "id_bnf \<equiv> (\<lambda>x. x)"
   165 
   166 lemma id_bnf_apply: "id_bnf x = x"
   167   unfolding id_bnf_def by simp
   168 
   169 bnf ID: 'a
   170   map: "id_bnf :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   171   sets: "\<lambda>x. {x}"
   172   bd: natLeq
   173   rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   174   pred: "id_bnf :: ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   175   unfolding id_bnf_def
   176   apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
   177   apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
   178   apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
   179   done
   180 
   181 lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
   182   unfolding id_bnf_def by unfold_locales auto
   183 
   184 ML_file "Tools/BNF/bnf_comp_tactics.ML"
   185 ML_file "Tools/BNF/bnf_comp.ML"
   186 ML_file "Tools/BNF/bnf_lift.ML"
   187 
   188 hide_fact
   189   DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0
   190   DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer
   191   DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq
   192   DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer
   193   ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id
   194   ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep
   195   ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer
   196 
   197 end