author | wenzelm |
Mon, 11 Sep 2023 19:30:48 +0200 | |
changeset 78659 | b5f3d1051b13 |
parent 76948 | f33df7529fed |
permissions | -rw-r--r-- |
49310 | 1 |
(* Title: HOL/Cardinals/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 |
|
48976 | 5 |
Well-order embeddings. |
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 |
|
63167 | 8 |
section \<open>Well-Order Embeddings\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
theory Wellorder_Embedding |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
11 |
imports Fun_More 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 |
|
63167 | 14 |
subsection \<open>Auxiliaries\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
lemma UNION_bij_betw_ofilter: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
17 |
assumes WELL: "Well_order r" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
18 |
OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
19 |
BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
20 |
shows "bij_betw f (\<Union>i \<in> I. A i) (\<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
|
21 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
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
|
23 |
hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
24 |
using wo_rel.ofilter_linord[of r] OF by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
with WELL BIJ show ?thesis |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
26 |
by (auto simp add: bij_betw_UNION_chain) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
|
63167 | 30 |
subsection \<open>(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible |
31 |
functions\<close> |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
lemma embed_halfcong: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
34 |
assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" and "embed r r' f" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
35 |
shows "embed r r' g" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
36 |
by (smt (verit, del_insts) assms bij_betw_cong embed_def in_mono under_Field) |
48975
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 embed_cong[fundef_cong]: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
39 |
assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
40 |
shows "embed r r' f = embed r r' g" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
41 |
by (metis assms embed_halfcong) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
lemma embedS_cong[fundef_cong]: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
44 |
assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
45 |
shows "embedS r r' f = embedS r r' g" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
46 |
unfolding embedS_def using assms |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
47 |
embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
lemma iso_cong[fundef_cong]: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
50 |
assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
51 |
shows "iso r r' f = iso r r' g" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
52 |
unfolding iso_def using assms |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
53 |
embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
lemma id_compat: "compat r r id" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
56 |
by(auto simp add: id_def compat_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
58 |
lemma comp_compat: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
59 |
"\<lbrakk>compat r r' f; compat r' r'' f'\<rbrakk> \<Longrightarrow> compat r r'' (f' o f)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
60 |
by(auto simp add: comp_def compat_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
corollary one_set_greater: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
63 |
"(\<exists>f::'a \<Rightarrow> 'a'. f ` A \<le> A' \<and> inj_on f A) \<or> (\<exists>g::'a' \<Rightarrow> 'a. g ` A' \<le> A \<and> inj_on g A')" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
obtain r where "well_order_on A r" by (fastforce simp add: well_order_on) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
hence 1: "A = Field r \<and> Well_order r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
67 |
using well_order_on_Well_order by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
69 |
hence 2: "A' = Field r' \<and> Well_order r'" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
70 |
using well_order_on_Well_order by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
hence "(\<exists>f. embed r r' f) \<or> (\<exists>g. embed r' r g)" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
72 |
using 1 2 by (auto simp add: wellorders_totally_ordered) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
{fix f assume "embed r r' f" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
75 |
hence "f`A \<le> A' \<and> inj_on f A" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
76 |
using 1 2 by (auto simp add: embed_Field embed_inj_on) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
{fix g assume "embed r' r g" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
80 |
hence "g`A' \<le> A \<and> inj_on g A'" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
81 |
using 1 2 by (auto simp add: embed_Field embed_inj_on) |
48975
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 |
ultimately show ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
corollary one_type_greater: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
87 |
"(\<exists>f::'a \<Rightarrow> 'a'. inj f) \<or> (\<exists>g::'a' \<Rightarrow> 'a. inj g)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
88 |
using one_set_greater[of UNIV UNIV] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
|
63167 | 91 |
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
|
92 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
lemma comp_embedS: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
94 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
95 |
and EMB: "embedS r r' f" and EMB': "embedS r' r'' f'" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
96 |
shows "embedS r r'' (f' o f)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
97 |
using EMB EMB' WELL WELL' embedS_comp_embed embedS_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
lemma iso_iff4: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
100 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
101 |
shows "iso r r' f = (embed r r' f \<and> embed r' r (inv_into (Field r) f))" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
102 |
using assms embed_bothWays_iso |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
103 |
by(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
lemma embed_embedS_iso: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
106 |
"embed r r' f = (embedS r r' f \<or> iso r r' f)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
107 |
unfolding embedS_def iso_def by blast |
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 not_embedS_iso: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
110 |
"\<not> (embedS r r' f \<and> iso r r' f)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
111 |
unfolding embedS_def iso_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
lemma embed_embedS_iff_not_iso: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
114 |
assumes "embed r r' f" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
115 |
shows "embedS r r' f = (\<not> iso r r' f)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
116 |
using assms unfolding embedS_def iso_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
118 |
lemma iso_inv_into: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
119 |
assumes WELL: "Well_order r" and ISO: "iso r r' f" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
120 |
shows "iso r' r (inv_into (Field r) f)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
121 |
by (meson ISO WELL bij_betw_inv_into inv_into_Field_embed_bij_betw iso_def iso_iff iso_iff2) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
123 |
lemma embedS_or_iso: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
124 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
125 |
shows "(\<exists>g. embedS r r' g) \<or> (\<exists>h. embedS r' r h) \<or> (\<exists>f. iso r r' f)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
126 |
by (metis WELL WELL' embed_embedS_iso embed_embedS_iso iso_iff4 wellorders_totally_ordered) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
127 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
128 |
end |