author | paulson <lp15@cam.ac.uk> |
Mon, 30 May 2022 12:46:11 +0100 | |
changeset 75494 | eded3fe9e600 |
parent 72125 | cf8399df4d76 |
child 76950 | f881fd264929 |
permissions | -rw-r--r-- |
55056 | 1 |
(* Title: HOL/BNF_Wellorder_Embedding.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
55059 | 5 |
Well-order embeddings as needed by bounded natural functors. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
60758 | 8 |
section \<open>Well-Order Embeddings as Needed by Bounded Natural Functors\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
55056 | 10 |
theory BNF_Wellorder_Embedding |
55936 | 11 |
imports Hilbert_Choice BNF_Wellorder_Relation |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
60758 | 14 |
text\<open>In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
prove their basic properties. The notion of embedding is considered from the point |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
of view of the theory of ordinals, and therefore requires the source to be injected |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
as an {\em initial segment} (i.e., {\em order filter}) of the target. A main result |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
of this section is the existence of embeddings (in one direction or another) between |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
any two well-orders, having as a consequence the fact that, given any two sets on |
60758 | 20 |
any two types, one is smaller than (i.e., can be injected into) the other.\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
|
60758 | 23 |
subsection \<open>Auxiliaries\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
lemma UNION_inj_on_ofilter: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
assumes WELL: "Well_order r" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)" |
60585 | 29 |
shows "inj_on f (\<Union>i \<in> I. A i)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
have "wo_rel r" using WELL by (simp add: wo_rel_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
using wo_rel.ofilter_linord[of r] OF by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
with WELL INJ show ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
by (auto simp add: inj_on_UNION_chain) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
lemma under_underS_bij_betw: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
41 |
BIJ: "bij_betw f (underS r a) (underS r' (f a))" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
42 |
shows "bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
proof- |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
44 |
have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
45 |
unfolding underS_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
{have "Refl r \<and> Refl r'" using WELL WELL' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
by (auto simp add: order_on_defs) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
49 |
hence "under r a = underS r a \<union> {a} \<and> |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
50 |
under r' (f a) = underS r' (f a) \<union> {f a}" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
51 |
using IN IN' by(auto simp add: Refl_under_underS) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
ultimately show ?thesis |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
54 |
using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
|
60758 | 58 |
subsection \<open>(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible |
59 |
functions\<close> |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
|
60758 | 61 |
text\<open>Standardly, a function is an embedding of a well-order in another if it injectively and |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
order-compatibly maps the former into an order filter of the latter. |
61799 | 63 |
Here we opt for a more succinct definition (operator \<open>embed\<close>), |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
asking that, for any element in the source, the function should be a bijection |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
between the set of strict lower bounds of that element |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
and the set of strict lower bounds of its image. (Later we prove equivalence with |
61799 | 67 |
the standard definition -- lemma \<open>embed_iff_compat_inj_on_ofilter\<close>.) |
68 |
A {\em strict embedding} (operator \<open>embedS\<close>) is a non-bijective embedding |
|
69 |
and an isomorphism (operator \<open>iso\<close>) is a bijective embedding.\<close> |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
where |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
73 |
"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
lemmas embed_defs = embed_def embed_def[abs_def] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
|
60758 | 77 |
text \<open>Strict embeddings:\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
"embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
lemmas embedS_defs = embedS_def embedS_def[abs_def] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
"iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
lemmas iso_defs = iso_def iso_def[abs_def] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
92 |
where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
"compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
lemma compat_wf: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
96 |
assumes CMP: "compat r r' f" and WF: "wf r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
97 |
shows "wf r" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
have "r \<le> inv_image r' f" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
100 |
unfolding inv_image_def using CMP |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
101 |
by (auto simp add: compat_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
102 |
with WF show ?thesis |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
103 |
using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
lemma id_embed: "embed r r id" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
107 |
by(auto simp add: id_def embed_def bij_betw_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
lemma id_iso: "iso r r id" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
110 |
by(auto simp add: id_def embed_def iso_def bij_betw_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
111 |
|
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
112 |
lemma embed_compat: |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
113 |
assumes EMB: "embed r r' f" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
114 |
shows "compat r r' f" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
115 |
unfolding compat_def |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
116 |
proof clarify |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
117 |
fix a b |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
118 |
assume *: "(a,b) \<in> r" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
119 |
hence 1: "b \<in> Field r" using Field_def[of r] by blast |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
120 |
have "a \<in> under r b" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
121 |
using * under_def[of r] by simp |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
122 |
hence "f a \<in> under r' (f b)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
123 |
using EMB embed_def[of r r' f] |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
124 |
bij_betw_def[of f "under r b" "under r' (f b)"] |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
125 |
image_def[of f "under r b"] 1 by auto |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
126 |
thus "(f a, f b) \<in> r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
127 |
by (auto simp add: under_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
128 |
qed |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
129 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
lemma embed_in_Field: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
131 |
assumes EMB: "embed r r' f" and IN: "a \<in> Field r" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
132 |
shows "f a \<in> Field r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
133 |
proof - |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
134 |
have "a \<in> Domain r \<or> a \<in> Range r" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
135 |
using IN unfolding Field_def by blast |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
136 |
then show ?thesis |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
137 |
using embed_compat [OF EMB] |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
138 |
unfolding Field_def compat_def by force |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
139 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
140 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
141 |
lemma comp_embed: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
142 |
assumes EMB: "embed r r' f" and EMB': "embed r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
143 |
shows "embed r r'' (f' \<circ> f)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
proof(unfold embed_def, auto) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
fix a assume *: "a \<in> Field r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
146 |
hence "bij_betw f (under r a) (under r' (f a))" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
147 |
using embed_def[of r] EMB by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
148 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
{have "f a \<in> Field r'" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
150 |
using EMB * by (auto simp add: embed_in_Field) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
151 |
hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
152 |
using embed_def[of r'] EMB' by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
ultimately |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
155 |
show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
156 |
by(auto simp add: bij_betw_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
157 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
158 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
lemma comp_iso: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
160 |
assumes EMB: "iso r r' f" and EMB': "iso r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
161 |
shows "iso r r'' (f' \<circ> f)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
162 |
using assms unfolding iso_def |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
163 |
by (auto simp add: comp_embed bij_betw_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
164 |
|
61799 | 165 |
text\<open>That \<open>embedS\<close> is also preserved by function composition shall be proved only later.\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
|
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
167 |
lemma embed_Field: "embed r r' f \<Longrightarrow> f`(Field r) \<le> Field r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
168 |
by (auto simp add: embed_in_Field) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
lemma embed_preserves_ofilter: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
171 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
EMB: "embed r r' f" and OF: "wo_rel.ofilter r A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
173 |
shows "wo_rel.ofilter r' (f`A)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
175 |
(* Preliminary facts *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
from WELL have Well: "wo_rel r" unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
177 |
from WELL' have Well': "wo_rel r'" unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
178 |
from OF have 0: "A \<le> Field r" by(auto simp add: Well wo_rel.ofilter_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
(* Main proof *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
proof(unfold wo_rel.ofilter_def, auto simp add: image_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
fix a b' |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
183 |
assume *: "a \<in> A" and **: "b' \<in> under r' (f a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
184 |
hence "a \<in> Field r" using 0 by auto |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
185 |
hence "bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
using * EMB by (auto simp add: embed_def) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
187 |
hence "f`(under r a) = under r' (f a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
by (simp add: bij_betw_def) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
189 |
with ** image_def[of f "under r a"] obtain b where |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
190 |
1: "b \<in> under r a \<and> b' = f b" by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
hence "b \<in> A" using Well * OF |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
192 |
by (auto simp add: wo_rel.ofilter_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
with 1 show "\<exists>b \<in> A. b' = f b" by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
194 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
197 |
lemma embed_Field_ofilter: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
198 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
199 |
EMB: "embed r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
200 |
shows "wo_rel.ofilter r' (f`(Field r))" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
201 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
have "wo_rel.ofilter r (Field r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
203 |
using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
204 |
with WELL WELL' EMB |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
show ?thesis by (auto simp add: embed_preserves_ofilter) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
206 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
lemma embed_inj_on: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
209 |
assumes WELL: "Well_order r" and EMB: "embed r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
210 |
shows "inj_on f (Field r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
proof(unfold inj_on_def, clarify) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
212 |
(* Preliminary facts *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
from WELL have Well: "wo_rel r" unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
with wo_rel.TOTAL[of r] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
have Total: "Total r" by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
from Well wo_rel.REFL[of r] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
have Refl: "Refl r" by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
(* Main proof *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
fix a b |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
assume *: "a \<in> Field r" and **: "b \<in> Field r" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
221 |
***: "f a = f b" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
hence 1: "a \<in> Field r \<and> b \<in> Field r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
unfolding Field_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
{assume "(a,b) \<in> r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
225 |
hence "a \<in> under r b \<and> b \<in> under r b" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
226 |
using Refl by(auto simp add: under_def refl_on_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
227 |
hence "a = b" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
228 |
using EMB 1 *** |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
by (auto simp add: embed_def bij_betw_def inj_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
231 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
232 |
{assume "(b,a) \<in> r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
233 |
hence "a \<in> under r a \<and> b \<in> under r a" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
234 |
using Refl by(auto simp add: under_def refl_on_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
hence "a = b" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
236 |
using EMB 1 *** |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
237 |
by (auto simp add: embed_def bij_betw_def inj_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
238 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
239 |
ultimately |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
240 |
show "a = b" using Total 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
241 |
by (auto simp add: total_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
242 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
243 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
244 |
lemma embed_underS: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
245 |
assumes WELL: "Well_order r" and |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
246 |
EMB: "embed r r' f" and IN: "a \<in> Field r" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
247 |
shows "bij_betw f (underS r a) (underS r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
248 |
proof- |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
249 |
have "f a \<in> Field r'" using assms embed_Field[of r r' f] by auto |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
250 |
then have 0: "under r a = underS r a \<union> {a}" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
251 |
by (simp add: IN Refl_under_underS WELL wo_rel.REFL wo_rel.intro) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
252 |
moreover have 1: "bij_betw f (under r a) (under r' (f a))" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
253 |
using assms by (auto simp add: embed_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
254 |
moreover have "under r' (f a) = underS r' (f a) \<union> {f a}" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
255 |
proof |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
256 |
show "under r' (f a) \<subseteq> underS r' (f a) \<union> {f a}" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
257 |
using underS_def under_def by fastforce |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
258 |
show "underS r' (f a) \<union> {f a} \<subseteq> under r' (f a)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
259 |
using bij_betwE 0 1 underS_subset_under by fastforce |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
260 |
qed |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
261 |
moreover have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
262 |
unfolding underS_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
263 |
ultimately show ?thesis |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
264 |
by (auto simp add: notIn_Un_bij_betw3) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
265 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
lemma embed_iff_compat_inj_on_ofilter: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
268 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f`(Field r)))" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
unfold embed_def, auto) (* get rid of one implication *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
273 |
fix a |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
274 |
assume *: "inj_on f (Field r)" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
275 |
**: "compat r r' f" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
276 |
***: "wo_rel.ofilter r' (f`(Field r))" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
277 |
****: "a \<in> Field r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
278 |
(* Preliminary facts *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
279 |
have Well: "wo_rel r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
280 |
using WELL wo_rel_def[of r] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
281 |
hence Refl: "Refl r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
282 |
using wo_rel.REFL[of r] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
283 |
have Total: "Total r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
284 |
using Well wo_rel.TOTAL[of r] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
285 |
have Well': "wo_rel r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
286 |
using WELL' wo_rel_def[of r'] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
287 |
hence Antisym': "antisym r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
288 |
using wo_rel.ANTISYM[of r'] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
289 |
have "(a,a) \<in> r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
using **** Well wo_rel.REFL[of r] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
291 |
refl_on_def[of _ r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
292 |
hence "(f a, f a) \<in> r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
293 |
using ** by(auto simp add: compat_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
294 |
hence 0: "f a \<in> Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
295 |
unfolding Field_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
296 |
have "f a \<in> f`(Field r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
297 |
using **** by auto |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
298 |
hence 2: "under r' (f a) \<le> f`(Field r)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
299 |
using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
300 |
(* Main proof *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
301 |
show "bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
302 |
proof(unfold bij_betw_def, auto) |
55811 | 303 |
show "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
304 |
next |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
305 |
fix b assume "b \<in> under r a" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
306 |
thus "f b \<in> under r' (f a)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
307 |
unfolding under_def using ** |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
308 |
by (auto simp add: compat_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
309 |
next |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
310 |
fix b' assume *****: "b' \<in> under r' (f a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
311 |
hence "b' \<in> f`(Field r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
using 2 by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
313 |
with Field_def[of r] obtain b where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
3: "b \<in> Field r" and 4: "b' = f b" by auto |
67613 | 315 |
have "(b,a) \<in> r" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
316 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
317 |
{assume "(a,b) \<in> r" |
67613 | 318 |
with ** 4 have "(f a, b') \<in> r'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
319 |
by (auto simp add: compat_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
with ***** Antisym' have "f a = b'" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
321 |
by(auto simp add: under_def antisym_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
322 |
with 3 **** 4 * have "a = b" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
323 |
by(auto simp add: inj_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
324 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
325 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
326 |
{assume "a = b" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
327 |
hence "(b,a) \<in> r" using Refl **** 3 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
328 |
by (auto simp add: refl_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
329 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
330 |
ultimately |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
331 |
show ?thesis using Total **** 3 by (fastforce simp add: total_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
332 |
qed |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
333 |
with 4 show "b' \<in> f`(under r a)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
334 |
unfolding under_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
335 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
336 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
337 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
338 |
lemma inv_into_ofilter_embed: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
339 |
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
340 |
BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
341 |
IMAGE: "f ` A = Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
342 |
shows "embed r' r (inv_into A f)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
343 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
344 |
(* Preliminary facts *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
345 |
have Well: "wo_rel r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
346 |
using WELL wo_rel_def[of r] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
347 |
have Refl: "Refl r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
348 |
using Well wo_rel.REFL[of r] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
349 |
have Total: "Total r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
350 |
using Well wo_rel.TOTAL[of r] by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
351 |
(* Main proof *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
352 |
have 1: "bij_betw f A (Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
353 |
proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
354 |
fix b1 b2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
355 |
assume *: "b1 \<in> A" and **: "b2 \<in> A" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
356 |
***: "f b1 = f b2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
357 |
have 11: "b1 \<in> Field r \<and> b2 \<in> Field r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
358 |
using * ** Well OF by (auto simp add: wo_rel.ofilter_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
359 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
360 |
{assume "(b1,b2) \<in> r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
361 |
hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
362 |
unfolding under_def using 11 Refl |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
363 |
by (auto simp add: refl_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
364 |
hence "b1 = b2" using BIJ * ** *** |
54482 | 365 |
by (simp add: bij_betw_def inj_on_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
366 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
367 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
368 |
{assume "(b2,b1) \<in> r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
369 |
hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
370 |
unfolding under_def using 11 Refl |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
371 |
by (auto simp add: refl_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
372 |
hence "b1 = b2" using BIJ * ** *** |
54482 | 373 |
by (simp add: bij_betw_def inj_on_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
374 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
375 |
ultimately |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
376 |
show "b1 = b2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
377 |
using Total by (auto simp add: total_on_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
378 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
379 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
380 |
let ?f' = "(inv_into A f)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
381 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
382 |
have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
383 |
proof(clarify) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
384 |
fix b assume *: "b \<in> A" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
385 |
hence "under r b \<le> A" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
386 |
using Well OF by(auto simp add: wo_rel.ofilter_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
387 |
moreover |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
388 |
have "f ` (under r b) = under r' (f b)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
389 |
using * BIJ by (auto simp add: bij_betw_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
390 |
ultimately |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
391 |
show "bij_betw ?f' (under r' (f b)) (under r b)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
392 |
using 1 by (auto simp add: bij_betw_inv_into_subset) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
393 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
394 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
395 |
have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
396 |
proof(clarify) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
397 |
fix b' assume *: "b' \<in> Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
398 |
have "b' = f (?f' b')" using * 1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
399 |
by (auto simp add: bij_betw_inv_into_right) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
400 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
401 |
{obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
402 |
hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
403 |
with 31 have "?f' b' \<in> A" by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
404 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
405 |
ultimately |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
406 |
show "bij_betw ?f' (under r' b') (under r (?f' b'))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
407 |
using 2 by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
408 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
409 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
410 |
thus ?thesis unfolding embed_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
411 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
412 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
413 |
lemma inv_into_underS_embed: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
414 |
assumes WELL: "Well_order r" and |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
415 |
BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
416 |
IN: "a \<in> Field r" and |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
417 |
IMAGE: "f ` (underS r a) = Field r'" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
418 |
shows "embed r' r (inv_into (underS r a) f)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
419 |
using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
420 |
by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
421 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
422 |
lemma inv_into_Field_embed: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
423 |
assumes WELL: "Well_order r" and EMB: "embed r r' f" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
424 |
IMAGE: "Field r' \<le> f ` (Field r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
425 |
shows "embed r' r (inv_into (Field r) f)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
426 |
proof- |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
427 |
have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
428 |
using EMB by (auto simp add: embed_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
429 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
430 |
have "f ` (Field r) \<le> Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
431 |
using EMB WELL by (auto simp add: embed_Field) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
432 |
ultimately |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
433 |
show ?thesis using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
434 |
by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
435 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
436 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
437 |
lemma inv_into_Field_embed_bij_betw: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
438 |
assumes EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
439 |
shows "embed r' r (inv_into (Field r) f)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
440 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
441 |
have "Field r' \<le> f ` (Field r)" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
442 |
using BIJ by (auto simp add: bij_betw_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
443 |
then have iso: "iso r r' f" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
444 |
by (simp add: BIJ EMB iso_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
445 |
have *: "\<forall>a. a \<in> Field r \<longrightarrow> bij_betw f (under r a) (under r' (f a))" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
446 |
using EMB embed_def by fastforce |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
447 |
show ?thesis |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
448 |
proof (clarsimp simp add: embed_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
449 |
fix a |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
450 |
assume a: "a \<in> Field r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
451 |
then have ar: "a \<in> f ` Field r" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
452 |
using BIJ bij_betw_imp_surj_on by blast |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
453 |
have [simp]: "f (inv_into (Field r) f a) = a" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
454 |
by (simp add: ar f_inv_into_f) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
455 |
show "bij_betw (inv_into (Field r) f) (under r' a) (under r (inv_into (Field r) f a))" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
456 |
proof (rule bij_betw_inv_into_subset [OF BIJ]) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
457 |
show "under r (inv_into (Field r) f a) \<subseteq> Field r" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
458 |
by (simp add: under_Field) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
459 |
have "inv_into (Field r) f a \<in> Field r" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
460 |
by (simp add: ar inv_into_into) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
461 |
then show "f ` under r (inv_into (Field r) f a) = under r' a" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
462 |
using bij_betw_imp_surj_on * by fastforce |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
463 |
qed |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
464 |
qed |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
465 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
466 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
467 |
|
60758 | 468 |
subsection \<open>Given any two well-orders, one can be embedded in the other\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
469 |
|
60758 | 470 |
text\<open>Here is an overview of the proof of of this fact, stated in theorem |
61799 | 471 |
\<open>wellorders_totally_ordered\<close>: |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
472 |
|
61799 | 473 |
Fix the well-orders \<open>r::'a rel\<close> and \<open>r'::'a' rel\<close>. |
474 |
Attempt to define an embedding \<open>f::'a \<Rightarrow> 'a'\<close> from \<open>r\<close> to \<open>r'\<close> in the |
|
475 |
natural way by well-order recursion ("hoping" that \<open>Field r\<close> turns out to be smaller |
|
476 |
than \<open>Field r'\<close>), but also record, at the recursive step, in a function |
|
477 |
\<open>g::'a \<Rightarrow> bool\<close>, the extra information of whether \<open>Field r'\<close> |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
478 |
gets exhausted or not. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
479 |
|
61799 | 480 |
If \<open>Field r'\<close> does not get exhausted, then \<open>Field r\<close> is indeed smaller |
481 |
and \<open>f\<close> is the desired embedding from \<open>r\<close> to \<open>r'\<close> |
|
482 |
(lemma \<open>wellorders_totally_ordered_aux\<close>). |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
483 |
|
61799 | 484 |
Otherwise, it means that \<open>Field r'\<close> is the smaller one, and the inverse of |
485 |
(the "good" segment of) \<open>f\<close> is the desired embedding from \<open>r'\<close> to \<open>r\<close> |
|
486 |
(lemma \<open>wellorders_totally_ordered_aux2\<close>). |
|
60758 | 487 |
\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
488 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
489 |
lemma wellorders_totally_ordered_aux: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
490 |
fixes r ::"'a rel" and r'::"'a' rel" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
491 |
f :: "'a \<Rightarrow> 'a'" and a::'a |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
492 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
493 |
IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
494 |
NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
495 |
shows "bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
496 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
497 |
(* Preliminary facts *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
498 |
have Well: "wo_rel r" using WELL unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
499 |
hence Refl: "Refl r" using wo_rel.REFL[of r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
500 |
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
501 |
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
502 |
have OF: "wo_rel.ofilter r (underS r a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
503 |
by (auto simp add: Well wo_rel.underS_ofilter) |
60585 | 504 |
hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
505 |
using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
506 |
(* Gather facts about elements of underS r a *) |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
507 |
{fix b assume *: "b \<in> underS r a" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
508 |
hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
509 |
have t1: "b \<in> Field r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
510 |
using * underS_Field[of r a] by auto |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
511 |
have t2: "f`(under r b) = under r' (f b)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
512 |
using IH * by (auto simp add: bij_betw_def) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
513 |
hence t3: "wo_rel.ofilter r' (f`(under r b))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
514 |
using Well' by (auto simp add: wo_rel.under_ofilter) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
515 |
have "f`(under r b) \<le> Field r'" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
516 |
using t2 by (auto simp add: under_Field) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
517 |
moreover |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
518 |
have "b \<in> under r b" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
519 |
using t1 by(auto simp add: Refl Refl_under_in) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
520 |
ultimately |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
521 |
have t4: "f b \<in> Field r'" by auto |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
522 |
have "f`(under r b) = under r' (f b) \<and> |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
523 |
wo_rel.ofilter r' (f`(under r b)) \<and> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
524 |
f b \<in> Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
525 |
using t2 t3 t4 by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
526 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
527 |
hence bFact: |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
528 |
"\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and> |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
529 |
wo_rel.ofilter r' (f`(under r b)) \<and> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
530 |
f b \<in> Field r'" by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
531 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
532 |
have subField: "f`(underS r a) \<le> Field r'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
533 |
using bFact by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
534 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
535 |
have OF': "wo_rel.ofilter r' (f`(underS r a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
536 |
proof- |
60585 | 537 |
have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
538 |
using UN by auto |
60585 | 539 |
also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast |
540 |
also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))" |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
541 |
using bFact by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
542 |
finally |
60585 | 543 |
have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" . |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
544 |
thus ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
545 |
using Well' bFact |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
546 |
wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
547 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
548 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
549 |
have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
550 |
using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
551 |
hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
552 |
using subField NOT by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
553 |
(* Main proof *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
554 |
have INCL1: "f`(underS r a) \<le> underS r' (f a) " |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
555 |
proof(auto) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
556 |
fix b assume *: "b \<in> underS r a" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
557 |
have "f b \<noteq> f a \<and> (f b, f a) \<in> r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
558 |
using subField Well' SUC NE * |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
559 |
wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
560 |
thus "f b \<in> underS r' (f a)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
561 |
unfolding underS_def by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
562 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
563 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
564 |
have INCL2: "underS r' (f a) \<le> f`(underS r a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
565 |
proof |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
566 |
fix b' assume "b' \<in> underS r' (f a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
567 |
hence "b' \<noteq> f a \<and> (b', f a) \<in> r'" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
568 |
unfolding underS_def by simp |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
569 |
thus "b' \<in> f`(underS r a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
570 |
using Well' SUC NE OF' |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
571 |
wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
572 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
573 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
574 |
have INJ: "inj_on f (underS r a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
575 |
proof- |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
576 |
have "\<forall>b \<in> underS r a. inj_on f (under r b)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
577 |
using IH by (auto simp add: bij_betw_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
578 |
moreover |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
579 |
have "\<forall>b. wo_rel.ofilter r (under r b)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
580 |
using Well by (auto simp add: wo_rel.under_ofilter) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
581 |
ultimately show ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
582 |
using WELL bFact UN |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
583 |
UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
584 |
by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
585 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
586 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
587 |
have BIJ: "bij_betw f (underS r a) (underS r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
588 |
unfolding bij_betw_def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
589 |
using INJ INCL1 INCL2 by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
590 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
591 |
have "f a \<in> Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
592 |
using Well' subField NE SUC |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
593 |
by (auto simp add: wo_rel.suc_inField) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
594 |
thus ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
595 |
using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
596 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
597 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
598 |
lemma wellorders_totally_ordered_aux2: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
599 |
fixes r ::"'a rel" and r'::"'a' rel" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
600 |
f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool" and a::'a |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
601 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
602 |
MAIN1: |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
603 |
"\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r' |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
604 |
\<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
605 |
\<and> |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
606 |
(\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r') |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
607 |
\<longrightarrow> g a = False)" and |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
608 |
MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow> |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
609 |
bij_betw f (under r a) (under r' (f a))" and |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
610 |
Case: "a \<in> Field r \<and> False \<in> g`(under r a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
611 |
shows "\<exists>f'. embed r' r f'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
612 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
613 |
have Well: "wo_rel r" using WELL unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
614 |
hence Refl: "Refl r" using wo_rel.REFL[of r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
615 |
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
616 |
have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
617 |
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
618 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
619 |
have 0: "under r a = underS r a \<union> {a}" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
620 |
using Refl Case by(auto simp add: Refl_under_underS) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
621 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
622 |
have 1: "g a = False" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
623 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
624 |
{assume "g a \<noteq> False" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
625 |
with 0 Case have "False \<in> g`(underS r a)" by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
626 |
with MAIN1 have "g a = False" by blast} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
627 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
628 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
629 |
let ?A = "{a \<in> Field r. g a = False}" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
630 |
let ?a = "(wo_rel.minim r ?A)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
631 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
632 |
have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
633 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
634 |
have 3: "False \<notin> g`(underS r ?a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
635 |
proof |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
636 |
assume "False \<in> g`(underS r ?a)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
637 |
then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
638 |
hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
639 |
by (auto simp add: underS_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
640 |
hence "b \<in> Field r" unfolding Field_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
641 |
with 31 have "b \<in> ?A" by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
642 |
hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
643 |
(* again: why worked without type annotations? *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
644 |
with 32 Antisym show False |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
645 |
by (auto simp add: antisym_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
646 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
647 |
have temp: "?a \<in> ?A" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
648 |
using Well 2 wo_rel.minim_in[of r ?A] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
649 |
hence 4: "?a \<in> Field r" by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
650 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
651 |
have 5: "g ?a = False" using temp by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
652 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
653 |
have 6: "f`(underS r ?a) = Field r'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
654 |
using MAIN1[of ?a] 3 5 by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
655 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
656 |
have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
657 |
proof |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
658 |
fix b assume as: "b \<in> underS r ?a" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
659 |
moreover |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
660 |
have "wo_rel.ofilter r (underS r ?a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
661 |
using Well by (auto simp add: wo_rel.underS_ofilter) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
662 |
ultimately |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
663 |
have "False \<notin> g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+ |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
664 |
moreover have "b \<in> Field r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
665 |
unfolding Field_def using as by (auto simp add: underS_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
666 |
ultimately |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
667 |
show "bij_betw f (under r b) (under r' (f b))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
668 |
using MAIN2 by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
669 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
670 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
671 |
have "embed r' r (inv_into (underS r ?a) f)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
672 |
using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
673 |
thus ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
674 |
unfolding embed_def by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
675 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
676 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
677 |
theorem wellorders_totally_ordered: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
678 |
fixes r ::"'a rel" and r'::"'a' rel" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
679 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
680 |
shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
681 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
682 |
(* Preliminary facts *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
683 |
have Well: "wo_rel r" using WELL unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
684 |
hence Refl: "Refl r" using wo_rel.REFL[of r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
685 |
have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
686 |
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
687 |
(* Main proof *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
688 |
obtain H where H_def: "H = |
67091 | 689 |
(\<lambda>h a. if False \<notin> (snd \<circ> h)`(underS r a) \<and> (fst \<circ> h)`(underS r a) \<noteq> Field r' |
690 |
then (wo_rel.suc r' ((fst \<circ> h)`(underS r a)), True) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
691 |
else (undefined, False))" by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
692 |
have Adm: "wo_rel.adm_wo r H" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
693 |
using Well |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
694 |
proof(unfold wo_rel.adm_wo_def, clarify) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
695 |
fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
696 |
assume "\<forall>y\<in>underS r x. h1 y = h2 y" |
67091 | 697 |
hence "\<forall>y\<in>underS r x. (fst \<circ> h1) y = (fst \<circ> h2) y \<and> |
698 |
(snd \<circ> h1) y = (snd \<circ> h2) y" by auto |
|
699 |
hence "(fst \<circ> h1)`(underS r x) = (fst \<circ> h2)`(underS r x) \<and> |
|
700 |
(snd \<circ> h1)`(underS r x) = (snd \<circ> h2)`(underS r x)" |
|
49922 | 701 |
by (auto simp add: image_def) |
702 |
thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
703 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
704 |
(* More constant definitions: *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
705 |
obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
706 |
where h_def: "h = wo_rel.worec r H" and |
67091 | 707 |
f_def: "f = fst \<circ> h" and g_def: "g = snd \<circ> h" by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
708 |
obtain test where test_def: |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
709 |
"test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
710 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
711 |
have *: "\<And> a. h a = H h a" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
712 |
using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
713 |
have Main1: |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
714 |
"\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
715 |
(\<not>(test a) \<longrightarrow> g a = False)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
716 |
proof- (* How can I prove this withou fixing a? *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
717 |
fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
718 |
(\<not>(test a) \<longrightarrow> g a = False)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
719 |
using *[of a] test_def f_def g_def H_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
720 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
721 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
722 |
let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow> |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
723 |
bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
724 |
have Main2: "\<And> a. ?phi a" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
725 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
726 |
fix a show "?phi a" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
727 |
proof(rule wo_rel.well_order_induct[of r ?phi], |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
728 |
simp only: Well, clarify) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
729 |
fix a |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
730 |
assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
731 |
*: "a \<in> Field r" and |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
732 |
**: "False \<notin> g`(under r a)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
733 |
have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
734 |
proof(clarify) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
735 |
fix b assume ***: "b \<in> underS r a" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
736 |
hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
737 |
moreover have "b \<in> Field r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
738 |
using *** underS_Field[of r a] by auto |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
739 |
moreover have "False \<notin> g`(under r b)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
740 |
using 0 ** Trans under_incr[of r b a] by auto |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
741 |
ultimately show "bij_betw f (under r b) (under r' (f b))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
742 |
using IH by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
743 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
744 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
745 |
have 21: "False \<notin> g`(underS r a)" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
746 |
using ** underS_subset_under[of r a] by auto |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
747 |
have 22: "g`(under r a) \<le> {True}" using ** by auto |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
748 |
moreover have 23: "a \<in> under r a" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
749 |
using Refl * by (auto simp add: Refl_under_in) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
750 |
ultimately have 24: "g a = True" by blast |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
751 |
have 2: "f`(underS r a) \<noteq> Field r'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
752 |
proof |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
753 |
assume "f`(underS r a) = Field r'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
754 |
hence "g a = False" using Main1 test_def by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
755 |
with 24 show False using ** by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
756 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
757 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
758 |
have 3: "f a = wo_rel.suc r' (f`(underS r a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
759 |
using 21 2 Main1 test_def by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
760 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
761 |
show "bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
762 |
using WELL WELL' 1 2 3 * |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
763 |
wellorders_totally_ordered_aux[of r r' a f] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
764 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
765 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
766 |
(* *) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
767 |
let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
768 |
show ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
769 |
proof(cases "\<exists>a. ?chi a") |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
770 |
assume "\<not> (\<exists>a. ?chi a)" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
771 |
hence "\<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
772 |
using Main2 by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
773 |
thus ?thesis unfolding embed_def by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
774 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
775 |
assume "\<exists>a. ?chi a" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
776 |
then obtain a where "?chi a" by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
777 |
hence "\<exists>f'. embed r' r f'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
778 |
using wellorders_totally_ordered_aux2[of r r' g f a] |
54482 | 779 |
WELL WELL' Main1 Main2 test_def by fast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
780 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
781 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
782 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
783 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
784 |
|
60758 | 785 |
subsection \<open>Uniqueness of embeddings\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
786 |
|
60758 | 787 |
text\<open>Here we show a fact complementary to the one from the previous subsection -- namely, |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
788 |
that between any two well-orders there is {\em at most} one embedding, and is the one |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
789 |
definable by the expected well-order recursive equation. As a consequence, any two |
60758 | 790 |
embeddings of opposite directions are mutually inverse.\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
791 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
792 |
lemma embed_determined: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
793 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
794 |
EMB: "embed r r' f" and IN: "a \<in> Field r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
795 |
shows "f a = wo_rel.suc r' (f`(underS r a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
796 |
proof- |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
797 |
have "bij_betw f (underS r a) (underS r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
798 |
using assms by (auto simp add: embed_underS) |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
799 |
hence "f`(underS r a) = underS r' (f a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
800 |
by (auto simp add: bij_betw_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
801 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
802 |
{have "f a \<in> Field r'" using IN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
803 |
using EMB WELL embed_Field[of r r' f] by auto |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
804 |
hence "f a = wo_rel.suc r' (underS r' (f a))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
805 |
using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
806 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
807 |
ultimately show ?thesis by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
808 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
809 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
810 |
lemma embed_unique: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
811 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
812 |
EMBf: "embed r r' f" and EMBg: "embed r r' g" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
813 |
shows "a \<in> Field r \<longrightarrow> f a = g a" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
814 |
proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
815 |
fix a |
67613 | 816 |
assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
817 |
*: "a \<in> Field r" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
818 |
hence "\<forall>b \<in> underS r a. f b = g b" |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
819 |
unfolding underS_def by (auto simp add: Field_def) |
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
55020
diff
changeset
|
820 |
hence "f`(underS r a) = g`(underS r a)" by force |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
821 |
thus "f a = g a" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
822 |
using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
823 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
824 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
825 |
lemma embed_bothWays_inverse: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
826 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
827 |
EMB: "embed r r' f" and EMB': "embed r' r f'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
828 |
shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
829 |
proof- |
67091 | 830 |
have "embed r r (f' \<circ> f)" using assms |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
831 |
by(auto simp add: comp_embed) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
832 |
moreover have "embed r r id" using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
833 |
by (auto simp add: id_embed) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
834 |
ultimately have "\<forall>a \<in> Field r. f'(f a) = a" |
67091 | 835 |
using assms embed_unique[of r r "f' \<circ> f" id] id_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
836 |
moreover |
67091 | 837 |
{have "embed r' r' (f \<circ> f')" using assms |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
838 |
by(auto simp add: comp_embed) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
839 |
moreover have "embed r' r' id" using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
840 |
by (auto simp add: id_embed) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
841 |
ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'" |
67091 | 842 |
using assms embed_unique[of r' r' "f \<circ> f'" id] id_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
843 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
844 |
ultimately show ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
845 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
846 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
847 |
lemma embed_bothWays_bij_betw: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
848 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
849 |
EMB: "embed r r' f" and EMB': "embed r' r g" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
850 |
shows "bij_betw f (Field r) (Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
851 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
852 |
let ?A = "Field r" let ?A' = "Field r'" |
67091 | 853 |
have "embed r r (g \<circ> f) \<and> embed r' r' (f \<circ> g)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
854 |
using assms by (auto simp add: comp_embed) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
855 |
hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')" |
67091 | 856 |
using WELL id_embed[of r] embed_unique[of r r "g \<circ> f" id] |
857 |
WELL' id_embed[of r'] embed_unique[of r' r' "f \<circ> g" id] |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
858 |
id_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
859 |
have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
860 |
using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
861 |
(* *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
862 |
show ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
863 |
proof(unfold bij_betw_def inj_on_def, auto simp add: 2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
864 |
fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
865 |
have "a = g(f a) \<and> b = g(f b)" using * 1 by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
866 |
with ** show "a = b" by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
867 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
868 |
fix a' assume *: "a' \<in> ?A'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
869 |
hence "g a' \<in> ?A \<and> f(g a') = a'" using 1 2 by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
870 |
thus "a' \<in> f ` ?A" by force |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
871 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
872 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
873 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
874 |
lemma embed_bothWays_iso: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
875 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
876 |
EMB: "embed r r' f" and EMB': "embed r' r g" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
877 |
shows "iso r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
878 |
unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
879 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
880 |
|
60758 | 881 |
subsection \<open>More properties of embeddings, strict embeddings and isomorphisms\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
882 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
883 |
lemma embed_bothWays_Field_bij_betw: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
884 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
885 |
EMB: "embed r r' f" and EMB': "embed r' r f'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
886 |
shows "bij_betw f (Field r) (Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
887 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
888 |
have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
889 |
using assms by (auto simp add: embed_bothWays_inverse) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
890 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
891 |
have "f`(Field r) \<le> Field r' \<and> f' ` (Field r') \<le> Field r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
892 |
using assms by (auto simp add: embed_Field) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
893 |
ultimately |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
894 |
show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
895 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
896 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
897 |
lemma embedS_comp_embed: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
898 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
899 |
and EMB: "embedS r r' f" and EMB': "embed r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
900 |
shows "embedS r r'' (f' \<circ> f)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
901 |
proof- |
67091 | 902 |
let ?g = "(f' \<circ> f)" let ?h = "inv_into (Field r) ?g" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
903 |
have 1: "embed r r' f \<and> \<not> (bij_betw f (Field r) (Field r'))" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
904 |
using EMB by (auto simp add: embedS_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
905 |
hence 2: "embed r r'' ?g" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
906 |
using EMB' comp_embed[of r r' f r'' f'] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
907 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
908 |
{assume "bij_betw ?g (Field r) (Field r'')" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
909 |
hence "embed r'' r ?h" using 2 |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
910 |
by (auto simp add: inv_into_Field_embed_bij_betw) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
911 |
hence "embed r' r (?h \<circ> f')" using EMB' |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
912 |
by (auto simp add: comp_embed) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
913 |
hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1 |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
914 |
by (auto simp add: embed_bothWays_Field_bij_betw) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
915 |
with 1 have False by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
916 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
917 |
ultimately show ?thesis unfolding embedS_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
918 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
919 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
920 |
lemma embed_comp_embedS: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
921 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
922 |
and EMB: "embed r r' f" and EMB': "embedS r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
923 |
shows "embedS r r'' (f' \<circ> f)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
924 |
proof- |
67091 | 925 |
let ?g = "(f' \<circ> f)" let ?h = "inv_into (Field r) ?g" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
926 |
have 1: "embed r' r'' f' \<and> \<not> (bij_betw f' (Field r') (Field r''))" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
927 |
using EMB' by (auto simp add: embedS_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
928 |
hence 2: "embed r r'' ?g" |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
929 |
using WELL EMB comp_embed[of r r' f r'' f'] by auto |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
930 |
moreover have \<section>: "f' ` Field r' \<subseteq> Field r''" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
931 |
by (simp add: "1" embed_Field) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
932 |
{assume \<section>: "bij_betw ?g (Field r) (Field r'')" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
933 |
hence "embed r'' r ?h" using 2 WELL |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
934 |
by (auto simp add: inv_into_Field_embed_bij_betw) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
935 |
hence "embed r' r (inv_into (Field r) ?g \<circ> f')" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
936 |
using "1" BNF_Wellorder_Embedding.comp_embed WELL' by blast |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
937 |
then have "bij_betw f' (Field r') (Field r'')" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
938 |
using EMB WELL WELL' \<section> bij_betw_comp_iff by (blast intro: embed_bothWays_Field_bij_betw) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
939 |
with 1 have False by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
940 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
941 |
ultimately show ?thesis unfolding embedS_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
942 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
943 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
944 |
lemma embed_comp_iso: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
945 |
assumes EMB: "embed r r' f" and EMB': "iso r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
946 |
shows "embed r r'' (f' \<circ> f)" using assms unfolding iso_def |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
947 |
by (auto simp add: comp_embed) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
948 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
949 |
lemma iso_comp_embed: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
950 |
assumes EMB: "iso r r' f" and EMB': "embed r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
951 |
shows "embed r r'' (f' \<circ> f)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
952 |
using assms unfolding iso_def by (auto simp add: comp_embed) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
953 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
954 |
lemma embedS_comp_iso: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
955 |
assumes EMB: "embedS r r' f" and EMB': "iso r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
956 |
shows "embedS r r'' (f' \<circ> f)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
957 |
proof - |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
958 |
have \<section>: "embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
959 |
using EMB embedS_def by blast |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
960 |
then have "embed r r'' (f' \<circ> f)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
961 |
using embed_comp_iso EMB' by blast |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
962 |
then have "f ` Field r \<subseteq> Field r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
963 |
by (simp add: embed_Field \<section>) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
964 |
then have "\<not> bij_betw (f' \<circ> f) (Field r) (Field r'')" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
965 |
using "\<section>" EMB' by (auto simp: bij_betw_comp_iff2 iso_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
966 |
then show ?thesis |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
967 |
by (simp add: \<open>embed r r'' (f' \<circ> f)\<close> embedS_def) |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
968 |
qed |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
969 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
970 |
lemma iso_comp_embedS: |
72125
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
971 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
972 |
and EMB: "iso r r' f" and EMB': "embedS r' r'' f'" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
973 |
shows "embedS r r'' (f' \<circ> f)" |
cf8399df4d76
elimination of some needless assumptions
paulson <lp15@cam.ac.uk>
parents:
72123
diff
changeset
|
974 |
using assms unfolding iso_def by (auto simp add: embed_comp_embedS) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
975 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
976 |
lemma embedS_Field: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
977 |
assumes WELL: "Well_order r" and EMB: "embedS r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
978 |
shows "f ` (Field r) < Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
979 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
980 |
have "f`(Field r) \<le> Field r'" using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
981 |
by (auto simp add: embed_Field embedS_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
982 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
983 |
{have "inj_on f (Field r)" using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
984 |
by (auto simp add: embedS_def embed_inj_on) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
985 |
hence "f`(Field r) \<noteq> Field r'" using EMB |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
986 |
by (auto simp add: embedS_def bij_betw_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
987 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
988 |
ultimately show ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
989 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
990 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
991 |
lemma embedS_iff: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
992 |
assumes WELL: "Well_order r" and ISO: "embed r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
993 |
shows "embedS r r' f = (f ` (Field r) < Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
994 |
proof |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
995 |
assume "embedS r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
996 |
thus "f ` Field r \<subset> Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
997 |
using WELL by (auto simp add: embedS_Field) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
998 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
999 |
assume "f ` Field r \<subset> Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1000 |
hence "\<not> bij_betw f (Field r) (Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1001 |
unfolding bij_betw_def by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1002 |
thus "embedS r r' f" unfolding embedS_def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1003 |
using ISO by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1004 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1005 |
|
72123 | 1006 |
lemma iso_Field: "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'" |
1007 |
by (auto simp add: iso_def bij_betw_def) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1008 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1009 |
lemma iso_iff: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1010 |
assumes "Well_order r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1011 |
shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1012 |
proof |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1013 |
assume "iso r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1014 |
thus "embed r r' f \<and> f ` (Field r) = Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1015 |
by (auto simp add: iso_Field iso_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1016 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1017 |
assume *: "embed r r' f \<and> f ` Field r = Field r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1018 |
hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1019 |
with * have "bij_betw f (Field r) (Field r')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1020 |
unfolding bij_betw_def by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1021 |
with * show "iso r r' f" unfolding iso_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1022 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1023 |
|
71857
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1024 |
lemma iso_iff2: "iso r r' f \<longleftrightarrow> |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1025 |
bij_betw f (Field r) (Field r') \<and> |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1026 |
(\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a, b) \<in> r \<longleftrightarrow> (f a, f b) \<in> r')" |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1027 |
(is "?lhs = ?rhs") |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1028 |
proof |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1029 |
assume L: ?lhs |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1030 |
then have "bij_betw f (Field r) (Field r')" and emb: "embed r r' f" |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1031 |
by (auto simp: bij_betw_def iso_def) |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1032 |
then obtain g where g: "\<And>x. x \<in> Field r \<Longrightarrow> g (f x) = x" |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1033 |
by (auto simp: bij_betw_iff_bijections) |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1034 |
moreover |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1035 |
have "(a, b) \<in> r" if "a \<in> Field r" "b \<in> Field r" "(f a, f b) \<in> r'" for a b |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1036 |
using that emb g g [OF FieldI1] \<comment>\<open>yes it's weird\<close> |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1037 |
by (force simp add: embed_def under_def bij_betw_iff_bijections) |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1038 |
ultimately show ?rhs |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1039 |
using L by (auto simp: compat_def iso_def dest: embed_compat) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1040 |
next |
71857
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1041 |
assume R: ?rhs |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1042 |
then show ?lhs |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1043 |
apply (clarsimp simp add: iso_def embed_def under_def bij_betw_iff_bijections) |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1044 |
apply (rule_tac x="g" in exI) |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1045 |
apply (fastforce simp add: intro: FieldI1)+ |
d73955442df5
a few new lemmas about functions
paulson <lp15@cam.ac.uk>
parents:
67613
diff
changeset
|
1046 |
done |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1047 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1048 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1049 |
lemma iso_iff3: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1050 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1051 |
shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1052 |
proof |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1053 |
assume "iso r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1054 |
thus "bij_betw f (Field r) (Field r') \<and> compat r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1055 |
unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1056 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1057 |
have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1058 |
by (auto simp add: wo_rel_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1059 |
assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1060 |
thus "iso r r' f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1061 |
unfolding "compat_def" using assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1062 |
proof(auto simp add: iso_iff2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1063 |
fix a b assume **: "a \<in> Field r" "b \<in> Field r" and |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1064 |
***: "(f a, f b) \<in> r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1065 |
{assume "(b,a) \<in> r \<or> b = a" |
67613 | 1066 |
hence "(b,a) \<in> r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1067 |
hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1068 |
hence "f a = f b" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1069 |
using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1070 |
hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1071 |
hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1072 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1073 |
thus "(a,b) \<in> r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1074 |
using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1075 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1076 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1077 |
|
72123 | 1078 |
lemma iso_imp_inj_on: |
1079 |
assumes "iso r r' f" shows "inj_on f (Field r)" |
|
1080 |
using assms unfolding iso_iff2 bij_betw_def by blast |
|
1081 |
||
1082 |
lemma iso_backward_Field: |
|
1083 |
assumes "x \<in> Field r'" "iso r r' f" |
|
1084 |
shows "inv_into (Field r) f x \<in> Field r" |
|
1085 |
using assms iso_Field by (blast intro!: inv_into_into) |
|
1086 |
||
1087 |
lemma iso_backward: |
|
1088 |
assumes "(x,y) \<in> r'" and iso: "iso r r' f" |
|
1089 |
shows "(inv_into (Field r) f x, inv_into (Field r) f y) \<in> r" |
|
1090 |
proof - |
|
1091 |
have \<section>: "\<And>x. (\<exists>xa\<in>Field r. x = f xa) = (x \<in> Field r')" |
|
1092 |
using assms iso_Field [OF iso] by (force simp add: ) |
|
1093 |
have "x \<in> Field r'" "y \<in> Field r'" |
|
1094 |
using assms by (auto simp: Field_def) |
|
1095 |
with \<section> [of x] \<section> [of y] assms show ?thesis |
|
1096 |
by (auto simp add: iso_iff2 bij_betw_inv_into_left) |
|
1097 |
qed |
|
1098 |
||
1099 |
lemma iso_forward: |
|
1100 |
assumes "(x,y) \<in> r" "iso r r' f" shows "(f x,f y) \<in> r'" |
|
1101 |
proof - |
|
1102 |
have "x \<in> Field r" "y \<in> Field r" |
|
1103 |
using assms by (auto simp: Field_def) |
|
1104 |
with assms show ?thesis unfolding iso_iff2 by blast |
|
1105 |
qed |
|
1106 |
||
1107 |
||
1108 |
lemma iso_trans: |
|
1109 |
assumes "trans r" and iso: "iso r r' f" shows "trans r'" |
|
1110 |
unfolding trans_def |
|
1111 |
proof clarify |
|
1112 |
fix x y z |
|
1113 |
assume xyz: "(x, y) \<in> r'" "(y, z) \<in> r'" |
|
1114 |
then have *: "(inv_into (Field r) f x, inv_into (Field r) f y) \<in> r" |
|
1115 |
"(inv_into (Field r) f y, inv_into (Field r) f z) \<in> r" |
|
1116 |
using iso_backward [OF _ iso] by blast+ |
|
1117 |
then have "inv_into (Field r) f x \<in> Field r" "inv_into (Field r) f y \<in> Field r" |
|
1118 |
by (auto simp: Field_def) |
|
1119 |
with * have "(inv_into (Field r) f x, inv_into (Field r) f z) \<in> r" |
|
1120 |
using assms(1) by (blast intro: transD) |
|
1121 |
then have "(f (inv_into (Field r) f x), f (inv_into (Field r) f z)) \<in> r'" |
|
1122 |
by (blast intro: iso iso_forward) |
|
1123 |
moreover have "x \<in> f ` Field r" "z \<in> f ` Field r" |
|
1124 |
using xyz iso iso_Field by (blast intro: FieldI1 FieldI2)+ |
|
1125 |
ultimately show "(x, z) \<in> r'" |
|
1126 |
by (simp add: f_inv_into_f) |
|
1127 |
qed |
|
1128 |
||
1129 |
lemma iso_Total: |
|
1130 |
assumes "Total r" and iso: "iso r r' f" shows "Total r'" |
|
1131 |
unfolding total_on_def |
|
1132 |
proof clarify |
|
1133 |
fix x y |
|
1134 |
assume xy: "x \<in> Field r'" "y \<in> Field r'" "x \<noteq> y" "(y,x) \<notin> r'" |
|
1135 |
then have \<section>: "inv_into (Field r) f x \<in> Field r" "inv_into (Field r) f y \<in> Field r" |
|
1136 |
using iso_backward_Field [OF _ iso] by auto |
|
1137 |
moreover have "x \<in> f ` Field r" "y \<in> f ` Field r" |
|
1138 |
using xy iso iso_Field by (blast intro: FieldI1 FieldI2)+ |
|
1139 |
ultimately have False if "inv_into (Field r) f x = inv_into (Field r) f y" |
|
1140 |
using inv_into_injective [OF that] \<open>x \<noteq> y\<close> by simp |
|
1141 |
then have "(inv_into (Field r) f x, inv_into (Field r) f y) \<in> r \<or> (inv_into (Field r) f y, inv_into (Field r) f x) \<in> r" |
|
1142 |
using assms \<section> by (auto simp: total_on_def) |
|
1143 |
then show "(x, y) \<in> r'" |
|
1144 |
using assms xy by (auto simp: iso_Field f_inv_into_f dest!: iso_forward [OF _ iso]) |
|
1145 |
qed |
|
1146 |
||
1147 |
lemma iso_wf: |
|
1148 |
assumes "wf r" and iso: "iso r r' f" shows "wf r'" |
|
1149 |
proof - |
|
1150 |
have "bij_betw f (Field r) (Field r')" |
|
1151 |
and iff: "(\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a, b) \<in> r \<longleftrightarrow> (f a, f b) \<in> r')" |
|
1152 |
using assms by (auto simp: iso_iff2) |
|
1153 |
show ?thesis |
|
1154 |
proof (rule wfI_min) |
|
1155 |
fix x::'b and Q |
|
1156 |
assume "x \<in> Q" |
|
1157 |
let ?g = "inv_into (Field r) f" |
|
1158 |
obtain z0 where "z0 \<in> ?g ` Q" |
|
1159 |
using \<open>x \<in> Q\<close> by blast |
|
1160 |
then obtain z where z: "z \<in> ?g ` Q" and "\<And>x y. \<lbrakk>(y, z) \<in> r; x \<in> Q\<rbrakk> \<Longrightarrow> y \<noteq> ?g x" |
|
1161 |
by (rule wfE_min [OF \<open>wf r\<close>]) auto |
|
1162 |
then have "\<forall>y. (y, inv_into Q ?g z) \<in> r' \<longrightarrow> y \<notin> Q" |
|
1163 |
by (clarsimp simp: f_inv_into_f[OF z] z dest!: iso_backward [OF _ iso]) blast |
|
1164 |
moreover have "inv_into Q ?g z \<in> Q" |
|
1165 |
by (simp add: inv_into_into z) |
|
1166 |
ultimately show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r' \<longrightarrow> y \<notin> Q" .. |
|
1167 |
qed |
|
1168 |
qed |
|
1169 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1170 |
end |