1 (* Title: HOL/BNF_Comp.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 header {* Composition of Bounded Natural Functors *} |
|
10 |
|
11 theory BNF_Comp |
|
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_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)" |
|
150 |
|
151 lemma id_bnf_comp_apply: "id_bnf_comp x = x" |
|
152 unfolding id_bnf_comp_def by simp |
|
153 |
|
154 bnf ID: 'a |
|
155 map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
156 sets: "\<lambda>x. {x}" |
|
157 bd: natLeq |
|
158 rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
159 unfolding id_bnf_comp_def |
|
160 apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) |
|
161 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
|
162 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] |
|
163 done |
|
164 |
|
165 lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV" |
|
166 unfolding id_bnf_comp_def by unfold_locales auto |
|
167 |
|
168 ML_file "Tools/BNF/bnf_comp_tactics.ML" |
|
169 ML_file "Tools/BNF/bnf_comp.ML" |
|
170 |
|
171 hide_const (open) id_bnf_comp |
|
172 hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV |
|
173 |
|
174 end |
|