equal
deleted
inserted
replaced
11 |
11 |
12 theory Basic_BNFs |
12 theory Basic_BNFs |
13 imports BNF_Def |
13 imports BNF_Def |
14 begin |
14 begin |
15 |
15 |
16 lemma wpull_id: "wpull UNIV B1 B2 id id id id" |
|
17 unfolding wpull_def by simp |
|
18 |
|
19 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq] |
16 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq] |
20 |
|
21 lemma ctwo_card_order: "card_order ctwo" |
|
22 using Card_order_ctwo by (unfold ctwo_def Field_card_of) |
|
23 |
17 |
24 lemma natLeq_cinfinite: "cinfinite natLeq" |
18 lemma natLeq_cinfinite: "cinfinite natLeq" |
25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
19 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
26 |
20 |
27 lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2" |
21 lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2" |
227 qed |
221 qed |
228 then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis |
222 then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis |
229 thus ?thesis using that by fastforce |
223 thus ?thesis using that by fastforce |
230 qed |
224 qed |
231 |
225 |
232 lemma card_of_bounded_range: |
|
233 "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|") |
|
234 proof - |
|
235 let ?f = "\<lambda>f. %x. if f x \<in> B then f x else undefined" |
|
236 have "inj_on ?f ?LHS" unfolding inj_on_def |
|
237 proof (unfold fun_eq_iff, safe) |
|
238 fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x |
|
239 assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x" |
|
240 hence "f x \<in> B" "g x \<in> B" by auto |
|
241 with eq have "Some (f x) = Some (g x)" by metis |
|
242 thus "f x = g x" by simp |
|
243 qed |
|
244 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce |
|
245 ultimately show ?thesis using card_of_ordLeq by fast |
|
246 qed |
|
247 |
|
248 bnf "'a \<Rightarrow> 'b" |
226 bnf "'a \<Rightarrow> 'b" |
249 map: "op \<circ>" |
227 map: "op \<circ>" |
250 sets: range |
228 sets: range |
251 bd: "natLeq +c |UNIV :: 'a set|" |
229 bd: "natLeq +c |UNIV :: 'a set|" |
252 rel: "fun_rel op =" |
230 rel: "fun_rel op =" |