author | blanchet |
Fri, 20 Dec 2013 20:36:38 +0100 | |
changeset 54838 | 16511f84913c |
parent 54581 | 1502a1f707d9 |
child 54841 | af71b753c459 |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49507
diff
changeset
|
1 |
(* Title: HOL/BNF/Basic_BNFs.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
|
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49236
diff
changeset
|
7 |
Registration of basic types as bounded natural functors. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49236
diff
changeset
|
10 |
header {* Registration of Basic Types as Bounded Natural Functors *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
theory Basic_BNFs |
49310 | 13 |
imports BNF_Def |
54581
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset
|
14 |
(*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*) |
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset
|
15 |
Lifting_Sum |
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset
|
16 |
Lifting_Product |
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset
|
17 |
Main |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
20 |
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" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
21 |
unfolding wpull_def Grp_def by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
22 |
|
54421 | 23 |
bnf ID: 'a |
24 |
map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
25 |
sets: "\<lambda>x. {x}" |
|
26 |
bd: natLeq |
|
27 |
rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
28 |
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
49453 | 30 |
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
done |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
|
54421 | 33 |
bnf DEADID: 'a |
34 |
map: "id :: 'a \<Rightarrow> 'a" |
|
35 |
bd: "natLeq +c |UNIV :: 'a set|" |
|
36 |
rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
37 |
by (auto simp add: wpull_Grp_def Grp_def |
51446 | 38 |
card_order_csum natLeq_card_order card_of_card_order_on |
39 |
cinfinite_csum natLeq_cinfinite) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
|
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
41 |
definition setl :: "'a + 'b \<Rightarrow> 'a set" where |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
42 |
"setl x = (case x of Inl z => {z} | _ => {})" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
|
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
44 |
definition setr :: "'a + 'b \<Rightarrow> 'b set" where |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
45 |
"setr x = (case x of Inr z => {z} | _ => {})" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
|
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
47 |
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
|
54421 | 49 |
bnf "'a + 'b" |
50 |
map: sum_map |
|
51 |
sets: setl setr |
|
52 |
bd: natLeq |
|
53 |
wits: Inl Inr |
|
54 |
rel: sum_rel |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
proof - |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
show "sum_map id id = id" by (rule sum_map.id) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
next |
54486 | 58 |
fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
by (rule sum_map.comp[symmetric]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
next |
54486 | 62 |
fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2 |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
63 |
assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
64 |
a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
thus "sum_map f1 f2 x = sum_map g1 g2 x" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
proof (cases x) |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
67 |
case Inl thus ?thesis using a1 by (clarsimp simp: setl_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
next |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
69 |
case Inr thus ?thesis using a2 by (clarsimp simp: setr_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
next |
54486 | 72 |
fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
73 |
show "setl o sum_map f1 f2 = image f1 o setl" |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
74 |
by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
next |
54486 | 76 |
fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
77 |
show "setr o sum_map f1 f2 = image f2 o setr" |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
78 |
by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
show "card_order natLeq" by (rule natLeq_card_order) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
show "cinfinite natLeq" by (rule natLeq_cinfinite) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
next |
54486 | 84 |
fix x :: "'o + 'p" |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
85 |
show "|setl x| \<le>o natLeq" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
apply (rule ordLess_imp_ordLeq) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
88 |
by (simp add: setl_def split: sum.split) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
next |
54486 | 90 |
fix x :: "'o + 'p" |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
91 |
show "|setr x| \<le>o natLeq" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
92 |
apply (rule ordLess_imp_ordLeq) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
94 |
by (simp add: setr_def split: sum.split) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
hence |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
pull1: "\<And>b1 b2. \<lbrakk>b1 \<in> B11; b2 \<in> B21; f11 b1 = f21 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A1. p11 a = b1 \<and> p21 a = b2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
100 |
and pull2: "\<And>b1 b2. \<lbrakk>b1 \<in> B12; b2 \<in> B22; f12 b1 = f22 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A2. p12 a = b1 \<and> p22 a = b2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
101 |
unfolding wpull_def by blast+ |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
102 |
show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2} |
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
103 |
{x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
(sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
(is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2") |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
proof (unfold wpull_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
{ fix B1 B2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
proof (cases B1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
case (Inl b1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
{ fix b2 assume "B2 = Inr b2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
with Inl *(3) have False by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
} then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
115 |
with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2" |
49451
7a28d22c33c6
renamed "sum_setl" to "setl" and similarly for r
blanchet
parents:
49450
diff
changeset
|
116 |
by (simp add: setl_def)+ |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
118 |
with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
119 |
by (simp add: sum_set_defs)+ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
121 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
case (Inr b1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
123 |
{ fix b2 assume "B2 = Inl b2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
124 |
with Inr *(3) have False by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
125 |
} then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
126 |
with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
127 |
by (simp add: sum_set_defs)+ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
128 |
with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
129 |
with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
by (simp add: sum_set_defs)+ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
(\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
136 |
qed |
49453 | 137 |
next |
138 |
fix R S |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
139 |
show "sum_rel R S = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
140 |
(Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
141 |
Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
142 |
unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff |
49453 | 143 |
by (fastforce split: sum.splits) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
qed (auto simp: sum_set_defs) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
"fsts x = {fst x}" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
148 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
"snds x = {snd x}" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
151 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
|
54421 | 154 |
bnf "'a \<times> 'b" |
155 |
map: map_pair |
|
156 |
sets: fsts snds |
|
157 |
bd: natLeq |
|
158 |
rel: prod_rel |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
proof (unfold prod_set_defs) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
160 |
show "map_pair id id = id" by (rule map_pair.id) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
161 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
162 |
fix f1 f2 g1 g2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
163 |
show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
164 |
by (rule map_pair.comp[symmetric]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
165 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
fix x f1 f2 g1 g2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
167 |
assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
168 |
thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
fix f1 f2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
171 |
show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
by (rule ext, unfold o_apply) simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
173 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
fix f1 f2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
175 |
show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
by (rule ext, unfold o_apply) simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
177 |
next |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
178 |
show "card_order natLeq" by (rule natLeq_card_order) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
next |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
180 |
show "cinfinite natLeq" by (rule natLeq_cinfinite) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
fix x |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
183 |
show "|{fst x}| \<le>o natLeq" |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
184 |
by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
next |
52635
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
186 |
fix x |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
187 |
show "|{snd x}| \<le>o natLeq" |
4f84b730c489
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents:
52545
diff
changeset
|
188 |
by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
189 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
192 |
thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
{x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
194 |
(map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
unfolding wpull_def by simp fast |
49453 | 196 |
next |
197 |
fix R S |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
198 |
show "prod_rel R S = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
199 |
(Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
200 |
Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
201 |
unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff |
49453 | 202 |
by auto |
54189
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53026
diff
changeset
|
203 |
qed |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
204 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
(* Categorical version of pullback: *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
206 |
lemma wpull_cat: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
assumes p: "wpull A B1 B2 f1 f2 p1 p2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
and c: "f1 o q1 = f2 o q2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
209 |
and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
210 |
obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
212 |
have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
proof safe |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
fix d |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
using p unfolding wpull_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
221 |
then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
thus ?thesis using that by fastforce |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
|
54421 | 225 |
bnf "'a \<Rightarrow> 'b" |
226 |
map: "op \<circ>" |
|
227 |
sets: range |
|
228 |
bd: "natLeq +c |UNIV :: 'a set|" |
|
229 |
rel: "fun_rel op =" |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
proof |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
231 |
fix f show "id \<circ> f = id f" by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
232 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
233 |
fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
unfolding comp_def[abs_def] .. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
236 |
fix x f g |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
237 |
assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
238 |
thus "f \<circ> x = g \<circ> x" by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
239 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
240 |
fix f show "range \<circ> op \<circ> f = op ` f \<circ> range" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
241 |
unfolding image_def comp_def[abs_def] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
242 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
243 |
show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)") |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
244 |
apply (rule card_order_csum) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
245 |
apply (rule natLeq_card_order) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
246 |
by (rule card_of_card_order_on) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
247 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
248 |
show "cinfinite (natLeq +c ?U)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
249 |
apply (rule cinfinite_csum) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
250 |
apply (rule disjI1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
251 |
by (rule natLeq_cinfinite) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
252 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
253 |
fix f :: "'d => 'a" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
254 |
have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image) |
54486 | 255 |
also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
256 |
finally show "|range f| \<le>o natLeq +c ?U" . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
257 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
258 |
fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
259 |
show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
260 |
(op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
261 |
unfolding wpull_def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
262 |
proof safe |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
263 |
fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
264 |
and c: "f1 \<circ> g1 = f2 \<circ> g2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
265 |
show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
using wpull_cat[OF p c r] by simp metis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
qed |
49453 | 268 |
next |
49463 | 269 |
fix R |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
270 |
show "fun_rel op = R = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
271 |
(Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
272 |
Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51836
diff
changeset
|
273 |
unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff |
54486 | 274 |
by auto (force, metis (no_types) pair_collapse) |
54189
c0186a0d8cb3
define a trivial nonemptiness witness if none is provided
traytel
parents:
53026
diff
changeset
|
275 |
qed |
54191 | 276 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
277 |
end |