src/HOL/BNF_Comp.thy
author blanchet
Sun May 04 18:14:58 2014 +0200 (2014-05-04)
changeset 56846 9df717fef2bb
parent 56166 9a241bc276cd
child 57698 afef6616cbae
permissions -rw-r--r--
renamed 'xxx_size' to 'size_xxx' for old datatype package
     1 (*  Title:      HOL/BNF_Comp.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Composition of bounded natural functors.
     6 *)
     7 
     8 header {* Composition of Bounded Natural Functors *}
     9 
    10 theory BNF_Comp
    11 imports BNF_Def
    12 begin
    13 
    14 lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
    15 by (rule ext) simp
    16 
    17 lemma Union_natural: "Union o image (image f) = image f o Union"
    18 by (rule ext) (auto simp only: comp_apply)
    19 
    20 lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    21 by (unfold comp_assoc)
    22 
    23 lemma comp_single_set_bd:
    24   assumes fbd_Card_order: "Card_order fbd" and
    25     fset_bd: "\<And>x. |fset x| \<le>o fbd" and
    26     gset_bd: "\<And>x. |gset x| \<le>o gbd"
    27   shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
    28 apply simp
    29 apply (rule ordLeq_transitive)
    30 apply (rule card_of_UNION_Sigma)
    31 apply (subst SIGMA_CSUM)
    32 apply (rule ordLeq_transitive)
    33 apply (rule card_of_Csum_Times')
    34 apply (rule fbd_Card_order)
    35 apply (rule ballI)
    36 apply (rule fset_bd)
    37 apply (rule ordLeq_transitive)
    38 apply (rule cprod_mono1)
    39 apply (rule gset_bd)
    40 apply (rule ordIso_imp_ordLeq)
    41 apply (rule ordIso_refl)
    42 apply (rule Card_order_cprod)
    43 done
    44 
    45 lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
    46 apply (erule ordIso_transitive)
    47 apply (frule csum_absorb2')
    48 apply (erule ordLeq_refl)
    49 by simp
    50 
    51 lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    52 apply (erule ordIso_transitive)
    53 apply (rule cprod_infinite)
    54 by simp
    55 
    56 lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
    57 by simp
    58 
    59 lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
    60 by simp
    61 
    62 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
    63 by (rule ext) (auto simp add: collect_def)
    64 
    65 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    66 by blast
    67 
    68 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    69 by blast
    70 
    71 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"
    72 by (unfold comp_apply collect_def) simp
    73 
    74 lemma wpull_cong:
    75 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
    76 by simp
    77 
    78 lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
    79 unfolding Grp_def fun_eq_iff relcompp.simps by auto
    80 
    81 lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
    82 by (rule arg_cong)
    83 
    84 lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
    85   vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
    86   unfolding vimage2p_def by auto
    87 
    88 lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x"
    89   by auto
    90 
    91 lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
    92   by auto
    93 
    94 lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
    95   by simp
    96 
    97 context
    98 fixes Rep Abs
    99 assumes type_copy: "type_definition Rep Abs UNIV"
   100 begin
   101 
   102 lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
   103   using type_definition.Rep_inverse[OF type_copy] by auto
   104 
   105 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)"
   106   using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   107 
   108 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)"
   109   using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
   110 
   111 lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
   112   using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   113 
   114 lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
   115     Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
   116   unfolding vimage2p_def Grp_def fun_eq_iff
   117   by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   118    type_definition.Rep_inverse[OF type_copy] dest: sym)
   119 
   120 lemma type_copy_vimage2p_Grp_Abs:
   121   "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
   122   unfolding vimage2p_def Grp_def fun_eq_iff
   123   by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   124    type_definition.Rep_inverse[OF type_copy] dest: sym)
   125 
   126 lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
   127 proof safe
   128   fix b assume "F b"
   129   show "\<exists>b'. F (Rep b')"
   130   proof (rule exI)
   131     from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
   132   qed
   133 qed blast
   134 
   135 lemma vimage2p_relcompp_converse:
   136   "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
   137   unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
   138   by (auto simp: type_copy_ex_RepI)
   139 
   140 end
   141 
   142 bnf DEADID: 'a
   143   map: "id :: 'a \<Rightarrow> 'a"
   144   bd: natLeq
   145   rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
   146 by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
   147 
   148 definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
   149 
   150 lemma id_bnf_comp_apply: "id_bnf_comp x = x"
   151   unfolding id_bnf_comp_def by simp
   152 
   153 bnf ID: 'a
   154   map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   155   sets: "\<lambda>x. {x}"
   156   bd: natLeq
   157   rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   158 unfolding id_bnf_comp_def
   159 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
   160 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
   161 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
   162 done
   163 
   164 lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
   165   unfolding id_bnf_comp_def by unfold_locales auto
   166 
   167 ML_file "Tools/BNF/bnf_comp_tactics.ML"
   168 ML_file "Tools/BNF/bnf_comp.ML"
   169 
   170 hide_const (open) id_bnf_comp
   171 hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
   172 
   173 end