src/HOL/Cardinals/Wellorder_Embedding.thy
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 76948 f33df7529fed
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49310
6e30078de4f0 renamed "Ordinals_and_Cardinals" to "Cardinals"
blanchet
parents: 48979
diff changeset
     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
2d17c305f4bc documentation cleanup
blanchet
parents: 48975
diff changeset
     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
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
     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
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
    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
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
    30
subsection \<open>(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
    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
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 60585
diff changeset
    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