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