src/HOL/BNF_Comp.thy
 author blanchet Sun Feb 23 22:51:11 2014 +0100 (2014-02-23) changeset 55705 a98a045a6169 parent 55066 4e5ddf3162ac child 55803 74d3fe9031d8 permissions -rw-r--r--
updated docs
```     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 Basic_BNFs
```
```    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 (subst sym[OF SUP_def])
```
```    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 Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
```
```    46 by simp
```
```    47
```
```    48 lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
```
```    49 by simp
```
```    50
```
```    51 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
```
```    52 by (rule ext) (auto simp add: collect_def)
```
```    53
```
```    54 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
```
```    55 by blast
```
```    56
```
```    57 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
```
```    58 by blast
```
```    59
```
```    60 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"
```
```    61 by (unfold comp_apply collect_def SUP_def)
```
```    62
```
```    63 lemma wpull_cong:
```
```    64 "\<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"
```
```    65 by simp
```
```    66
```
```    67 lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
```
```    68 unfolding Grp_def fun_eq_iff relcompp.simps by auto
```
```    69
```
```    70 lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
```
```    71 by (rule arg_cong)
```
```    72
```
```    73 ML_file "Tools/BNF/bnf_comp_tactics.ML"
```
```    74 ML_file "Tools/BNF/bnf_comp.ML"
```
```    75
```
```    76 end
```