author | paulson <lp15@cam.ac.uk> |
Thu, 12 Jan 2023 17:12:36 +0000 | |
changeset 76946 | 5df58a471d9e |
parent 75624 | 22d1c5f2b9f4 |
child 76948 | f33df7529fed |
permissions | -rw-r--r-- |
58127
b7cab82f488e
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
blanchet
parents:
55102
diff
changeset
|
1 |
(* Title: HOL/Cardinals/Wellorder_Constructions.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 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
Constructions on wellorders. |
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>Constructions on Wellorders\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
58127
b7cab82f488e
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
blanchet
parents:
55102
diff
changeset
|
10 |
theory Wellorder_Constructions |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
11 |
imports |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
12 |
Wellorder_Embedding Order_Union |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
|
70078 | 15 |
unbundle cardinal_syntax |
16 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
declare |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
ordLeq_Well_order_simp[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
not_ordLeq_iff_ordLess[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
not_ordLess_iff_ordLeq[simp] |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
21 |
Func_empty[simp] |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
22 |
Func_is_emp[simp] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
|
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 |
|
63167 | 26 |
subsection \<open>Order filters versus restrictions and embeddings\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
lemma ofilter_subset_iso: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
29 |
assumes WELL: "Well_order r" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
30 |
OFA: "ofilter r A" and OFB: "ofilter r B" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
31 |
shows "(A = B) = iso (Restr r A) (Restr r B) id" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
32 |
using assms by (auto simp add: ofilter_subset_embedS_iso) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
|
63167 | 35 |
subsection \<open>Ordering the well-orders by existence of embeddings\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
corollary ordLeq_refl_on: "refl_on {r. Well_order r} ordLeq" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
38 |
using ordLeq_reflexive unfolding ordLeq_def refl_on_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
39 |
by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
corollary ordLeq_trans: "trans ordLeq" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
42 |
using trans_def[of ordLeq] ordLeq_transitive by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
corollary ordLeq_preorder_on: "preorder_on {r. Well_order r} ordLeq" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
45 |
by(auto simp add: preorder_on_def ordLeq_refl_on ordLeq_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
corollary ordIso_refl_on: "refl_on {r. Well_order r} ordIso" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
48 |
using ordIso_reflexive unfolding refl_on_def ordIso_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
49 |
by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
corollary ordIso_trans: "trans ordIso" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
52 |
using trans_def[of ordIso] ordIso_transitive by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
corollary ordIso_sym: "sym ordIso" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
55 |
by (auto simp add: sym_def ordIso_symmetric) |
48975
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 |
corollary ordIso_equiv: "equiv {r. Well_order r} ordIso" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
58 |
by (auto simp add: equiv_def ordIso_sym ordIso_refl_on ordIso_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
|
54476 | 60 |
lemma ordLess_Well_order_simp[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
61 |
assumes "r <o r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
62 |
shows "Well_order r \<and> Well_order r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
63 |
using assms unfolding ordLess_def by simp |
54476 | 64 |
|
65 |
lemma ordIso_Well_order_simp[simp]: |
|
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
66 |
assumes "r =o r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
67 |
shows "Well_order r \<and> Well_order r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
68 |
using assms unfolding ordIso_def by simp |
54476 | 69 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
lemma ordLess_irrefl: "irrefl ordLess" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
71 |
by(unfold irrefl_def, auto simp add: ordLess_irreflexive) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
lemma ordLess_or_ordIso: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
74 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
75 |
shows "r <o r' \<or> r' <o r \<or> r =o r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
76 |
unfolding ordLess_def ordIso_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
77 |
using assms embedS_or_iso[of r r'] by auto |
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 |
corollary ordLeq_ordLess_Un_ordIso: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
80 |
"ordLeq = ordLess \<union> ordIso" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
81 |
by (auto simp add: ordLeq_iff_ordLess_or_ordIso) |
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 |
lemma ordIso_or_ordLess: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
84 |
assumes WELL: "Well_order r" and WELL': "Well_order r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
85 |
shows "r =o r' \<or> r <o r' \<or> r' <o r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
86 |
using assms ordLess_or_ordLeq ordLeq_iff_ordLess_or_ordIso by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
lemmas ord_trans = ordIso_transitive ordLeq_transitive ordLess_transitive |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
89 |
ordIso_ordLeq_trans ordLeq_ordIso_trans |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
90 |
ordIso_ordLess_trans ordLess_ordIso_trans |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
91 |
ordLess_ordLeq_trans ordLeq_ordLess_trans |
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 ofilter_ordLeq: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
94 |
assumes "Well_order r" and "ofilter r A" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
95 |
shows "Restr r A \<le>o r" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
have "A \<le> Field r" using assms by (auto simp add: wo_rel_def wo_rel.ofilter_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
thus ?thesis using assms |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
99 |
by (simp add: ofilter_subset_ordLeq wo_rel.Field_ofilter |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
100 |
wo_rel_def Restr_Field) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
101 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
102 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
corollary under_Restr_ordLeq: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
104 |
"Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
105 |
by (auto simp add: ofilter_ordLeq wo_rel.under_ofilter wo_rel_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
|
63167 | 108 |
subsection \<open>Copy via direct images\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
lemma Id_dir_image: "dir_image Id f \<le> Id" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
111 |
unfolding dir_image_def by auto |
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 Un_dir_image: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
114 |
"dir_image (r1 \<union> r2) f = (dir_image r1 f) \<union> (dir_image r2 f)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
115 |
unfolding dir_image_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
116 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
lemma Int_dir_image: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
118 |
assumes "inj_on f (Field r1 \<union> Field r2)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
119 |
shows "dir_image (r1 Int r2) f = (dir_image r1 f) Int (dir_image r2 f)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
proof |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
121 |
show "dir_image (r1 Int r2) f \<le> (dir_image r1 f) Int (dir_image r2 f)" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
122 |
using assms unfolding dir_image_def inj_on_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
123 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
124 |
show "(dir_image r1 f) Int (dir_image r2 f) \<le> dir_image (r1 Int r2) f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
125 |
proof(clarify) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
126 |
fix a' b' |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
127 |
assume "(a',b') \<in> dir_image r1 f" "(a',b') \<in> dir_image r2 f" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
128 |
then obtain a1 b1 a2 b2 |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
129 |
where 1: "a' = f a1 \<and> b' = f b1 \<and> a' = f a2 \<and> b' = f b2" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
130 |
2: "(a1,b1) \<in> r1 \<and> (a2,b2) \<in> r2" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
131 |
3: "{a1,b1} \<le> Field r1 \<and> {a2,b2} \<le> Field r2" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
132 |
unfolding dir_image_def Field_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
hence "a1 = a2 \<and> b1 = b2" using assms unfolding inj_on_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
hence "a' = f a1 \<and> b' = f b1 \<and> (a1,b1) \<in> r1 Int r2 \<and> (a2,b2) \<in> r1 Int r2" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
135 |
using 1 2 by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
136 |
thus "(a',b') \<in> dir_image (r1 \<inter> r2) f" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
137 |
unfolding dir_image_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
qed |
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 |
|
52203
055c392e79cf
fixed broken Cardinals and BNF due to Order_Union
popescua
parents:
52183
diff
changeset
|
141 |
(* More facts on ordinal sum: *) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
142 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
lemma Osum_embed: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
144 |
assumes FLD: "Field r Int Field r' = {}" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
145 |
WELL: "Well_order r" and WELL': "Well_order r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
146 |
shows "embed r (r Osum r') id" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
148 |
have 1: "Well_order (r Osum r')" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
149 |
using assms by (auto simp add: Osum_Well_order) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
151 |
have "compat r (r Osum r') id" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
152 |
unfolding compat_def Osum_def by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
have "inj_on id (Field r)" by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
155 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
156 |
have "ofilter (r Osum r') (Field r)" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
157 |
using 1 proof(auto simp add: wo_rel_def wo_rel.ofilter_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
158 |
Field_Osum under_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
fix a b assume 2: "a \<in> Field r" and 3: "(b,a) \<in> r Osum r'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
160 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
161 |
{assume "(b,a) \<in> r'" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
162 |
hence "a \<in> Field r'" using Field_def[of r'] by blast |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
163 |
hence False using 2 FLD by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
164 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
165 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
{assume "a \<in> Field r'" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
167 |
hence False using 2 FLD by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
168 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
ultimately |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
show "b \<in> Field r" by (auto simp add: Osum_def Field_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
171 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
ultimately show ?thesis |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
173 |
using assms by (auto simp add: embed_iff_compat_inj_on_ofilter) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
175 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
corollary Osum_ordLeq: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
177 |
assumes FLD: "Field r Int Field r' = {}" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
178 |
WELL: "Well_order r" and WELL': "Well_order r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
179 |
shows "r \<le>o r Osum r'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
180 |
using assms Osum_embed Osum_Well_order |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
181 |
unfolding ordLeq_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
183 |
lemma Well_order_embed_copy: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
184 |
assumes WELL: "well_order_on A r" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
185 |
INJ: "inj_on f A" and SUB: "f ` A \<le> B" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
186 |
shows "\<exists>r'. well_order_on B r' \<and> r \<le>o r'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
187 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
have "bij_betw f A (f ` A)" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
189 |
using INJ inj_on_imp_bij_betw by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
then obtain r'' where "well_order_on (f ` A) r''" and 1: "r =o r''" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
191 |
using WELL Well_order_iso_copy by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
192 |
hence 2: "Well_order r'' \<and> Field r'' = (f ` A)" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
193 |
using well_order_on_Well_order by blast |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
194 |
(* *) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
let ?C = "B - (f ` A)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
obtain r''' where "well_order_on ?C r'''" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
197 |
using well_order_on by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
198 |
hence 3: "Well_order r''' \<and> Field r''' = ?C" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
199 |
using well_order_on_Well_order by blast |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
200 |
(* *) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
201 |
let ?r' = "r'' Osum r'''" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
have "Field r'' Int Field r''' = {}" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
203 |
using 2 3 by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
204 |
hence "r'' \<le>o ?r'" using Osum_ordLeq[of r'' r'''] 2 3 by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
hence 4: "r \<le>o ?r'" using 1 ordIso_ordLeq_trans by blast |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
206 |
(* *) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
hence "Well_order ?r'" unfolding ordLeq_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
209 |
have "Field ?r' = B" using 2 3 SUB by (auto simp add: Field_Osum) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
210 |
ultimately show ?thesis using 4 by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
212 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
|
63167 | 214 |
subsection \<open>The maxim among a finite set of ordinals\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
|
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
216 |
text \<open>The correct phrasing would be ``a maxim of \<dots>", as \<open>\<le>o\<close> is only a preorder.\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
definition isOmax :: "'a rel set \<Rightarrow> 'a rel \<Rightarrow> bool" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
219 |
where |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
220 |
"isOmax R r \<equiv> r \<in> R \<and> (\<forall>r' \<in> R. r' \<le>o r)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
221 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
definition omax :: "'a rel set \<Rightarrow> 'a rel" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
223 |
where |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
224 |
"omax R == SOME r. isOmax R r" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
225 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
lemma exists_isOmax: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
227 |
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
228 |
shows "\<exists> r. isOmax R r" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
have "finite R \<Longrightarrow> R \<noteq> {} \<longrightarrow> (\<forall> r \<in> R. Well_order r) \<longrightarrow> (\<exists> r. isOmax R r)" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
231 |
apply(erule finite_induct) apply(simp add: isOmax_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
232 |
proof(clarsimp) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
233 |
fix r :: "('a \<times> 'a) set" and R assume *: "finite R" and **: "r \<notin> R" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
234 |
and ***: "Well_order r" and ****: "\<forall>r\<in>R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
235 |
and IH: "R \<noteq> {} \<longrightarrow> (\<exists>p. isOmax R p)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
236 |
let ?R' = "insert r R" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
237 |
show "\<exists>p'. (isOmax ?R' p')" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
238 |
proof(cases "R = {}") |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
239 |
case True |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
240 |
thus ?thesis unfolding isOmax_def using *** |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
241 |
by (simp add: ordLeq_reflexive) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
242 |
next |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
243 |
case False |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
244 |
then obtain p where p: "isOmax R p" using IH by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
245 |
hence 1: "Well_order p" using **** unfolding isOmax_def by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
246 |
{assume Case21: "r \<le>o p" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
247 |
hence "isOmax ?R' p" using p unfolding isOmax_def by simp |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
248 |
hence ?thesis by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
249 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
250 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
251 |
{assume Case22: "p \<le>o r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
252 |
{fix r' assume "r' \<in> ?R'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
253 |
moreover |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
254 |
{assume "r' \<in> R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
255 |
hence "r' \<le>o p" using p unfolding isOmax_def by simp |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
256 |
hence "r' \<le>o r" using Case22 by(rule ordLeq_transitive) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
257 |
} |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
258 |
moreover have "r \<le>o r" using *** by(rule ordLeq_reflexive) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
259 |
ultimately have "r' \<le>o r" by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
260 |
} |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
261 |
hence "isOmax ?R' r" unfolding isOmax_def by simp |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
262 |
hence ?thesis by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
263 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
264 |
moreover have "r \<le>o p \<or> p \<le>o r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
265 |
using 1 *** ordLeq_total by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
ultimately show ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
268 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
thus ?thesis using assms by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
lemma omax_isOmax: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
273 |
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
274 |
shows "isOmax R (omax R)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
275 |
unfolding omax_def using assms |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
276 |
by(simp add: exists_isOmax someI_ex) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
277 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
278 |
lemma omax_in: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
279 |
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
280 |
shows "omax R \<in> R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
281 |
using assms omax_isOmax unfolding isOmax_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
282 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
283 |
lemma Well_order_omax: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
284 |
assumes "finite R" and "R \<noteq> {}" and "\<forall>r\<in>R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
285 |
shows "Well_order (omax R)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
286 |
using assms omax_in by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
287 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
288 |
lemma omax_maxim: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
289 |
assumes "finite R" and "\<forall> r \<in> R. Well_order r" and "r \<in> R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
290 |
shows "r \<le>o omax R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
291 |
using assms omax_isOmax unfolding isOmax_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
292 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
293 |
lemma omax_ordLeq: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
294 |
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. r \<le>o p" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
295 |
shows "omax R \<le>o p" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
296 |
by (meson assms omax_in ordLeq_Well_order_simp) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
297 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
298 |
lemma omax_ordLess: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
299 |
assumes "finite R" and "R \<noteq> {}" and "\<forall> r \<in> R. r <o p" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
300 |
shows "omax R <o p" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
301 |
by (meson assms omax_in ordLess_Well_order_simp) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
302 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
303 |
lemma omax_ordLeq_elim: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
304 |
assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
305 |
and "omax R \<le>o p" and "r \<in> R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
306 |
shows "r \<le>o p" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
307 |
by (meson assms omax_maxim ordLeq_transitive) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
308 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
309 |
lemma omax_ordLess_elim: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
310 |
assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
311 |
and "omax R <o p" and "r \<in> R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
312 |
shows "r <o p" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
313 |
by (meson assms omax_maxim ordLeq_ordLess_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
315 |
lemma ordLeq_omax: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
316 |
assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
317 |
and "r \<in> R" and "p \<le>o r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
318 |
shows "p \<le>o omax R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
319 |
by (meson assms omax_maxim ordLeq_transitive) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
lemma ordLess_omax: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
322 |
assumes "finite R" and "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
323 |
and "r \<in> R" and "p <o r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
324 |
shows "p <o omax R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
325 |
by (meson assms omax_maxim ordLess_ordLeq_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
326 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
327 |
lemma omax_ordLeq_mono: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
328 |
assumes P: "finite P" and R: "finite R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
329 |
and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
330 |
and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p \<le>o r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
331 |
shows "omax P \<le>o omax R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
332 |
by (meson LEQ NE_P P R Well_R omax_ordLeq ordLeq_omax) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
333 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
334 |
lemma omax_ordLess_mono: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
335 |
assumes P: "finite P" and R: "finite R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
336 |
and NE_P: "P \<noteq> {}" and Well_R: "\<forall> r \<in> R. Well_order r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
337 |
and LEQ: "\<forall> p \<in> P. \<exists> r \<in> R. p <o r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
338 |
shows "omax P <o omax R" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
339 |
by (meson LEQ NE_P P R Well_R omax_ordLess ordLess_omax) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
340 |
|
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
341 |
|
63167 | 342 |
subsection \<open>Limit and succesor ordinals\<close> |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
343 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
344 |
lemma embed_underS2: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
345 |
assumes r: "Well_order r" and g: "embed r s g" and a: "a \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
346 |
shows "g ` underS r a = underS s (g a)" |
72126
5de9a5fbf2ec
adjustments for fewer WO assumptions
paulson <lp15@cam.ac.uk>
parents:
70078
diff
changeset
|
347 |
by (meson a bij_betw_def embed_underS g r) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
348 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
349 |
lemma bij_betw_insert: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
350 |
assumes "b \<notin> A" and "f b \<notin> A'" and "bij_betw f A A'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
351 |
shows "bij_betw f (insert b A) (insert (f b) A')" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
352 |
using notIn_Un_bij_betw[OF assms] by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
353 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
354 |
context wo_rel |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
355 |
begin |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
356 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
357 |
lemma underS_induct: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
358 |
assumes "\<And>a. (\<And> a1. a1 \<in> underS a \<Longrightarrow> P a1) \<Longrightarrow> P a" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
359 |
shows "P a" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
360 |
by (induct rule: well_order_induct) (rule assms, simp add: underS_def) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
361 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
362 |
lemma suc_underS: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
363 |
assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
364 |
shows "b \<in> underS (suc B)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
365 |
using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
366 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
367 |
lemma underS_supr: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
368 |
assumes bA: "b \<in> underS (supr A)" and A: "A \<subseteq> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
369 |
shows "\<exists> a \<in> A. b \<in> underS a" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
370 |
proof(rule ccontr, simp) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
371 |
have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
372 |
assume "\<forall>a\<in>A. b \<notin> underS a" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
373 |
hence 0: "\<forall>a \<in> A. (a,b) \<in> r" using A bA unfolding underS_def |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
374 |
by simp (metis REFL in_mono max2_def max2_greater refl_on_domain) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
375 |
have "(supr A, b) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
376 |
by (simp add: "0" A bb supr_least) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
377 |
thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
378 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
379 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
380 |
lemma underS_suc: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
381 |
assumes bA: "b \<in> underS (suc A)" and A: "A \<subseteq> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
382 |
shows "\<exists> a \<in> A. b \<in> under a" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
383 |
proof(rule ccontr, simp) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
384 |
have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
385 |
assume "\<forall>a\<in>A. b \<notin> under a" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
386 |
hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
387 |
by (metis bb in_mono max2_def max2_greater mem_Collect_eq underS_I under_def) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
388 |
have "(suc A, b) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
389 |
by (metis "0" A bb suc_least underS_E) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
390 |
thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
391 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
392 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
393 |
lemma (in wo_rel) in_underS_supr: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
394 |
assumes j: "j \<in> underS i" and i: "i \<in> A" and A: "A \<subseteq> Field r" and AA: "Above A \<noteq> {}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
395 |
shows "j \<in> underS (supr A)" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
396 |
proof- |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
397 |
have "(i,supr A) \<in> r" using supr_greater[OF A AA i] . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
398 |
thus ?thesis using j unfolding underS_def |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
399 |
by simp (metis REFL TRANS max2_def max2_equals1 refl_on_domain transD) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
400 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
401 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
402 |
lemma inj_on_Field: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
403 |
assumes A: "A \<subseteq> Field r" and f: "\<And> a b. \<lbrakk>a \<in> A; b \<in> A; a \<in> underS b\<rbrakk> \<Longrightarrow> f a \<noteq> f b" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
404 |
shows "inj_on f A" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
405 |
by (smt (verit) A f in_notinI inj_on_def subsetD underS_I) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
406 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
407 |
lemma ofilter_init_seg_of: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
408 |
assumes "ofilter F" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
409 |
shows "Restr r F initial_segment_of r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
410 |
using assms unfolding ofilter_def init_seg_of_def under_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
411 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
412 |
lemma underS_init_seg_of_Collect: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
413 |
assumes "\<And>j1 j2. \<lbrakk>j2 \<in> underS i; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
414 |
shows "{R j |j. j \<in> underS i} \<in> Chains init_seg_of" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
415 |
unfolding Chains_def proof safe |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
416 |
fix j ja assume jS: "j \<in> underS i" and jaS: "ja \<in> underS i" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
417 |
and init: "(R ja, R j) \<notin> init_seg_of" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
418 |
hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
419 |
and jjai: "(j,i) \<in> r" "(ja,i) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
420 |
and i: "i \<notin> {j,ja}" unfolding Field_def underS_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
421 |
have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+ |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
422 |
show "R j initial_segment_of R ja" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
423 |
using jja init TOTALS assms jS jaS by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
424 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
425 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
426 |
lemma (in wo_rel) Field_init_seg_of_Collect: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
427 |
assumes "\<And>j1 j2. \<lbrakk>j2 \<in> Field r; (j1, j2) \<in> r\<rbrakk> \<Longrightarrow> R j1 initial_segment_of R j2" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
428 |
shows "{R j |j. j \<in> Field r} \<in> Chains init_seg_of" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
429 |
unfolding Chains_def proof safe |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
430 |
fix j ja assume jS: "j \<in> Field r" and jaS: "ja \<in> Field r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
431 |
and init: "(R ja, R j) \<notin> init_seg_of" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
432 |
hence jja: "{j,ja} \<subseteq> Field r" and j: "j \<in> Field r" and ja: "ja \<in> Field r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
433 |
unfolding Field_def underS_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
434 |
have jj: "(j,j) \<in> r" and jaja: "(ja,ja) \<in> r" using j ja by (metis in_notinI)+ |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
435 |
show "R j initial_segment_of R ja" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
436 |
using TOTALS assms init jS jaS by blast |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
437 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
438 |
|
63167 | 439 |
subsubsection \<open>Successor and limit elements of an ordinal\<close> |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
440 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
441 |
definition "succ i \<equiv> suc {i}" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
442 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
443 |
definition "isSucc i \<equiv> \<exists> j. aboveS j \<noteq> {} \<and> i = succ j" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
444 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
445 |
definition "zero = minim (Field r)" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
446 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
447 |
definition "isLim i \<equiv> \<not> isSucc i" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
448 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
449 |
lemma zero_smallest[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
450 |
assumes "j \<in> Field r" shows "(zero, j) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
451 |
unfolding zero_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
452 |
by (metis AboveS_Field assms subset_AboveS_UnderS subset_antisym subset_refl suc_def suc_least_AboveS) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
453 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
454 |
lemma zero_in_Field: assumes "Field r \<noteq> {}" shows "zero \<in> Field r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
455 |
using assms unfolding zero_def by (metis Field_ofilter minim_in ofilter_def) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
456 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
457 |
lemma leq_zero_imp[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
458 |
"(x, zero) \<in> r \<Longrightarrow> x = zero" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
459 |
by (metis ANTISYM WELL antisymD well_order_on_domain zero_smallest) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
460 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
461 |
lemma leq_zero[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
462 |
assumes "Field r \<noteq> {}" shows "(x, zero) \<in> r \<longleftrightarrow> x = zero" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
463 |
using zero_in_Field[OF assms] in_notinI[of x zero] by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
464 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
465 |
lemma under_zero[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
466 |
assumes "Field r \<noteq> {}" shows "under zero = {zero}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
467 |
using assms unfolding under_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
468 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
469 |
lemma underS_zero[simp,intro]: "underS zero = {}" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
470 |
unfolding underS_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
471 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
472 |
lemma isSucc_succ: "aboveS i \<noteq> {} \<Longrightarrow> isSucc (succ i)" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
473 |
unfolding isSucc_def succ_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
474 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
475 |
lemma succ_in_diff: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
476 |
assumes "aboveS i \<noteq> {}" shows "(i,succ i) \<in> r \<and> succ i \<noteq> i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
477 |
using assms suc_greater[of "{i}"] unfolding succ_def AboveS_def aboveS_def Field_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
478 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
479 |
lemmas succ_in[simp] = succ_in_diff[THEN conjunct1] |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
480 |
lemmas succ_diff[simp] = succ_in_diff[THEN conjunct2] |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
481 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
482 |
lemma succ_in_Field[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
483 |
assumes "aboveS i \<noteq> {}" shows "succ i \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
484 |
using succ_in[OF assms] unfolding Field_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
485 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
486 |
lemma succ_not_in: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
487 |
assumes "aboveS i \<noteq> {}" shows "(succ i, i) \<notin> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
488 |
by (metis FieldI2 assms max2_equals1 max2_equals2 succ_diff succ_in) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
489 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
490 |
lemma not_isSucc_zero: "\<not> isSucc zero" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
491 |
by (metis isSucc_def leq_zero_imp succ_in_diff) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
492 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
493 |
lemma isLim_zero[simp]: "isLim zero" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
494 |
by (metis isLim_def not_isSucc_zero) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
495 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
496 |
lemma succ_smallest: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
497 |
assumes "(i,j) \<in> r" and "i \<noteq> j" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
498 |
shows "(succ i, j) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
499 |
unfolding succ_def apply(rule suc_least) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
500 |
using assms unfolding Field_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
501 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
502 |
lemma isLim_supr: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
503 |
assumes f: "i \<in> Field r" and l: "isLim i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
504 |
shows "i = supr (underS i)" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
505 |
proof(rule equals_supr) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
506 |
fix j assume j: "j \<in> Field r" and 1: "\<And> j'. j' \<in> underS i \<Longrightarrow> (j',j) \<in> r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
507 |
show "(i,j) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
508 |
proof(intro in_notinI[OF _ f j], safe) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
509 |
assume ji: "(j,i) \<in> r" "j \<noteq> i" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
510 |
hence a: "aboveS j \<noteq> {}" unfolding aboveS_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
511 |
hence "i \<noteq> succ j" using l unfolding isLim_def isSucc_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
512 |
moreover have "(succ j, i) \<in> r" using succ_smallest[OF ji] by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
513 |
ultimately have "succ j \<in> underS i" unfolding underS_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
514 |
hence "(succ j, j) \<in> r" using 1 by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
515 |
thus False using succ_not_in[OF a] by simp |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
516 |
qed |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
517 |
qed(use f underS_def Field_def in fastforce)+ |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
518 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
519 |
definition "pred i \<equiv> SOME j. j \<in> Field r \<and> aboveS j \<noteq> {} \<and> succ j = i" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
520 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
521 |
lemma pred_Field_succ: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
522 |
assumes "isSucc i" shows "pred i \<in> Field r \<and> aboveS (pred i) \<noteq> {} \<and> succ (pred i) = i" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
523 |
proof- |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
524 |
obtain j where j: "aboveS j \<noteq> {}" "i = succ j" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
525 |
using assms unfolding isSucc_def by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
526 |
then obtain "j \<in> Field r" "j \<noteq> i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
527 |
by (metis FieldI1 succ_diff succ_in) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
528 |
then show ?thesis unfolding pred_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
529 |
by (metis (mono_tags, lifting) j someI_ex) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
530 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
531 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
532 |
lemmas pred_Field[simp] = pred_Field_succ[THEN conjunct1] |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
533 |
lemmas aboveS_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct1] |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
534 |
lemmas succ_pred[simp] = pred_Field_succ[THEN conjunct2, THEN conjunct2] |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
535 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
536 |
lemma isSucc_pred_in: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
537 |
assumes "isSucc i" shows "(pred i, i) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
538 |
by (metis assms pred_Field_succ succ_in) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
539 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
540 |
lemma isSucc_pred_diff: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
541 |
assumes "isSucc i" shows "pred i \<noteq> i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
542 |
by (metis aboveS_pred assms succ_diff succ_pred) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
543 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
544 |
(* todo: pred maximal, pred injective? *) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
545 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
546 |
lemma succ_inj[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
547 |
assumes "aboveS i \<noteq> {}" and "aboveS j \<noteq> {}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
548 |
shows "succ i = succ j \<longleftrightarrow> i = j" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
549 |
by (metis FieldI1 assms succ_def succ_in supr_under under_underS_suc) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
550 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
551 |
lemma pred_succ[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
552 |
assumes "aboveS j \<noteq> {}" shows "pred (succ j) = j" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
553 |
using assms isSucc_def pred_Field_succ succ_inj by blast |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
554 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
555 |
lemma less_succ[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
556 |
assumes "aboveS i \<noteq> {}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
557 |
shows "(j, succ i) \<in> r \<longleftrightarrow> (j,i) \<in> r \<or> j = succ i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
558 |
by (metis FieldI1 assms in_notinI max2_equals1 max2_equals2 max2_iff succ_in succ_smallest) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
559 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
560 |
lemma underS_succ[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
561 |
assumes "aboveS i \<noteq> {}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
562 |
shows "underS (succ i) = under i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
563 |
unfolding underS_def under_def by (auto simp: assms succ_not_in) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
564 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
565 |
lemma succ_mono: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
566 |
assumes "aboveS j \<noteq> {}" and "(i,j) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
567 |
shows "(succ i, succ j) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
568 |
by (metis (full_types) assms less_succ succ_smallest) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
569 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
570 |
lemma under_succ[simp]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
571 |
assumes "aboveS i \<noteq> {}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
572 |
shows "under (succ i) = insert (succ i) (under i)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
573 |
using less_succ[OF assms] unfolding under_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
574 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
575 |
definition mergeSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
576 |
where |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
577 |
"mergeSL S L f i \<equiv> if isSucc i then S (pred i) (f (pred i)) else L f i" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
578 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
579 |
|
63167 | 580 |
subsubsection \<open>Well-order recursion with (zero), succesor, and limit\<close> |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
581 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
582 |
definition worecSL :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
583 |
where "worecSL S L \<equiv> worec (mergeSL S L)" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
584 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
585 |
definition "adm_woL L \<equiv> \<forall>f g i. isLim i \<and> (\<forall>j\<in>underS i. f j = g j) \<longrightarrow> L f i = L g i" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
586 |
|
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
587 |
lemma mergeSL: "adm_woL L \<Longrightarrow>adm_wo (mergeSL S L)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
588 |
unfolding adm_wo_def adm_woL_def isLim_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
589 |
by (smt (verit, ccfv_threshold) isSucc_pred_diff isSucc_pred_in mergeSL_def underS_I) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
590 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
591 |
lemma worec_fixpoint1: "adm_wo H \<Longrightarrow> worec H i = H (worec H) i" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
592 |
by (metis worec_fixpoint) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
593 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
594 |
lemma worecSL_isSucc: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
595 |
assumes a: "adm_woL L" and i: "isSucc i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
596 |
shows "worecSL S L i = S (pred i) (worecSL S L (pred i))" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
597 |
by (metis a i mergeSL mergeSL_def worecSL_def worec_fixpoint) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
598 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
599 |
lemma worecSL_succ: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
600 |
assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
601 |
shows "worecSL S L (succ j) = S j (worecSL S L j)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
602 |
by (simp add: a i isSucc_succ worecSL_isSucc) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
603 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
604 |
lemma worecSL_isLim: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
605 |
assumes a: "adm_woL L" and i: "isLim i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
606 |
shows "worecSL S L i = L (worecSL S L) i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
607 |
by (metis a i isLim_def mergeSL mergeSL_def worecSL_def worec_fixpoint) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
608 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
609 |
definition worecZSL :: "'b \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
610 |
where "worecZSL Z S L \<equiv> worecSL S (\<lambda> f a. if a = zero then Z else L f a)" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
611 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
612 |
lemma worecZSL_zero: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
613 |
assumes a: "adm_woL L" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
614 |
shows "worecZSL Z S L zero = Z" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
615 |
by (smt (verit, best) adm_woL_def assms isLim_zero worecSL_isLim worecZSL_def) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
616 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
617 |
lemma worecZSL_succ: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
618 |
assumes a: "adm_woL L" and i: "aboveS j \<noteq> {}" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
619 |
shows "worecZSL Z S L (succ j) = S j (worecZSL Z S L j)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
620 |
unfolding worecZSL_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
621 |
by (smt (verit, best) a adm_woL_def i worecSL_succ) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
622 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
623 |
lemma worecZSL_isLim: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
624 |
assumes a: "adm_woL L" and "isLim i" and "i \<noteq> zero" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
625 |
shows "worecZSL Z S L i = L (worecZSL Z S L) i" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
626 |
proof- |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
627 |
let ?L = "\<lambda> f a. if a = zero then Z else L f a" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
628 |
have "worecZSL Z S L i = ?L (worecZSL Z S L) i" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
629 |
unfolding worecZSL_def by (smt (verit, best) adm_woL_def assms worecSL_isLim) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
630 |
also have "\<dots> = L (worecZSL Z S L) i" using assms by simp |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
631 |
finally show ?thesis . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
632 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
633 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
634 |
|
63167 | 635 |
subsubsection \<open>Well-order succ-lim induction\<close> |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
636 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
637 |
lemma ord_cases: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
638 |
obtains j where "i = succ j" and "aboveS j \<noteq> {}" | "isLim i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
639 |
by (metis isLim_def isSucc_def) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
640 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
641 |
lemma well_order_inductSL[case_names Suc Lim]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
642 |
assumes "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" "\<And>i. \<lbrakk>isLim i; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
643 |
shows "P i" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
644 |
proof(induction rule: well_order_induct) |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
645 |
case (1 x) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
646 |
then show ?case |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
647 |
by (metis assms ord_cases succ_diff succ_in underS_E) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
648 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
649 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
650 |
lemma well_order_inductZSL[case_names Zero Suc Lim]: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
651 |
assumes "P zero" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
652 |
and "\<And>i. \<lbrakk>aboveS i \<noteq> {}; P i\<rbrakk> \<Longrightarrow> P (succ i)" and |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
653 |
"\<And>i. \<lbrakk>isLim i; i \<noteq> zero; \<And>j. j \<in> underS i \<Longrightarrow> P j\<rbrakk> \<Longrightarrow> P i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
654 |
shows "P i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
655 |
by (metis assms well_order_inductSL) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
656 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
657 |
(* Succesor and limit ordinals *) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
658 |
definition "isSuccOrd \<equiv> \<exists> j \<in> Field r. \<forall> i \<in> Field r. (i,j) \<in> r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
659 |
definition "isLimOrd \<equiv> \<not> isSuccOrd" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
660 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
661 |
lemma isLimOrd_succ: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
662 |
assumes isLimOrd and "i \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
663 |
shows "succ i \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
664 |
using assms unfolding isLimOrd_def isSuccOrd_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
665 |
by (metis REFL in_notinI refl_on_domain succ_smallest) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
666 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
667 |
lemma isLimOrd_aboveS: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
668 |
assumes l: isLimOrd and i: "i \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
669 |
shows "aboveS i \<noteq> {}" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
670 |
proof- |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
671 |
obtain j where "j \<in> Field r" and "(j,i) \<notin> r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
672 |
using assms unfolding isLimOrd_def isSuccOrd_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
673 |
hence "(i,j) \<in> r \<and> j \<noteq> i" by (metis i max2_def max2_greater) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
674 |
thus ?thesis unfolding aboveS_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
675 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
676 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
677 |
lemma succ_aboveS_isLimOrd: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
678 |
assumes "\<forall> i \<in> Field r. aboveS i \<noteq> {} \<and> succ i \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
679 |
shows isLimOrd |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
680 |
using assms isLimOrd_def isSuccOrd_def succ_not_in by blast |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
681 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
682 |
lemma isLim_iff: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
683 |
assumes l: "isLim i" and j: "j \<in> underS i" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
684 |
shows "\<exists> k. k \<in> underS i \<and> j \<in> underS k" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
685 |
by (metis Order_Relation.underS_Field empty_iff isLim_supr j l underS_empty underS_supr) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
686 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
687 |
end (* context wo_rel *) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
688 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
689 |
abbreviation "zero \<equiv> wo_rel.zero" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
690 |
abbreviation "succ \<equiv> wo_rel.succ" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
691 |
abbreviation "pred \<equiv> wo_rel.pred" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
692 |
abbreviation "isSucc \<equiv> wo_rel.isSucc" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
693 |
abbreviation "isLim \<equiv> wo_rel.isLim" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
694 |
abbreviation "isLimOrd \<equiv> wo_rel.isLimOrd" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
695 |
abbreviation "isSuccOrd \<equiv> wo_rel.isSuccOrd" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
696 |
abbreviation "adm_woL \<equiv> wo_rel.adm_woL" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
697 |
abbreviation "worecSL \<equiv> wo_rel.worecSL" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
698 |
abbreviation "worecZSL \<equiv> wo_rel.worecZSL" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
699 |
|
55102 | 700 |
|
63167 | 701 |
subsection \<open>Projections of wellorders\<close> |
58127
b7cab82f488e
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
blanchet
parents:
55102
diff
changeset
|
702 |
|
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
703 |
definition "oproj r s f \<equiv> Field s \<subseteq> f ` (Field r) \<and> compat r s f" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
704 |
|
58127
b7cab82f488e
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
blanchet
parents:
55102
diff
changeset
|
705 |
lemma oproj_in: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
706 |
assumes "oproj r s f" and "(a,a') \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
707 |
shows "(f a, f a') \<in> s" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
708 |
using assms unfolding oproj_def compat_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
709 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
710 |
lemma oproj_Field: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
711 |
assumes f: "oproj r s f" and a: "a \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
712 |
shows "f a \<in> Field s" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
713 |
using oproj_in[OF f] a unfolding Field_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
714 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
715 |
lemma oproj_Field2: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
716 |
assumes f: "oproj r s f" and a: "b \<in> Field s" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
717 |
shows "\<exists> a \<in> Field r. f a = b" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
718 |
using assms unfolding oproj_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
719 |
|
58127
b7cab82f488e
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
blanchet
parents:
55102
diff
changeset
|
720 |
lemma oproj_under: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
721 |
assumes f: "oproj r s f" and a: "a \<in> under r a'" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
722 |
shows "f a \<in> under s (f a')" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
723 |
using oproj_in[OF f] a unfolding under_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
724 |
|
58127
b7cab82f488e
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
blanchet
parents:
55102
diff
changeset
|
725 |
(* An ordinal is embedded in another whenever it is embedded as an order |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
726 |
(not necessarily as initial segment):*) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
727 |
theorem embedI: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
728 |
assumes r: "Well_order r" and s: "Well_order s" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
729 |
and f: "\<And> a. a \<in> Field r \<Longrightarrow> f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
730 |
shows "\<exists> g. embed r s g" |
58127
b7cab82f488e
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
blanchet
parents:
55102
diff
changeset
|
731 |
proof- |
61605 | 732 |
interpret r: wo_rel r by unfold_locales (rule r) |
733 |
interpret s: wo_rel s by unfold_locales (rule s) |
|
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
734 |
let ?G = "\<lambda> g a. suc s (g ` underS r a)" |
63040 | 735 |
define g where "g = worec r ?G" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
736 |
have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
737 |
(* *) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
738 |
{fix a assume "a \<in> Field r" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
739 |
hence "bij_betw g (under r a) (under s (g a)) \<and> |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
740 |
g a \<in> under s (f a)" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
741 |
proof(induction a rule: r.underS_induct) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
742 |
case (1 a) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
743 |
hence a: "a \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
744 |
and IH1a: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> inj_on g (under r a1)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
745 |
and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
746 |
and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
747 |
unfolding underS_def Field_def bij_betw_def by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
748 |
have fa: "f a \<in> Field s" using f[OF a] by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
749 |
have g: "g a = suc s (g ` underS r a)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
750 |
using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
751 |
have A0: "g ` underS r a \<subseteq> Field s" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
752 |
using IH1b by (metis IH2 image_subsetI in_mono under_Field) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
753 |
{fix a1 assume a1: "a1 \<in> underS r a" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
754 |
from IH2[OF this] have "g a1 \<in> under s (f a1)" . |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
755 |
moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
756 |
ultimately have "g a1 \<in> underS s (f a)" by (metis s.ANTISYM s.TRANS under_underS_trans) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
757 |
} |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
758 |
hence "f a \<in> AboveS s (g ` underS r a)" unfolding AboveS_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
759 |
using fa by simp (metis (lifting, full_types) mem_Collect_eq underS_def) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
760 |
hence A: "AboveS s (g ` underS r a) \<noteq> {}" by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
761 |
have B: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> underS s (g a)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
762 |
unfolding g apply(rule s.suc_underS[OF A0 A]) by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
763 |
{fix a1 a2 assume a2: "a2 \<in> underS r a" and 1: "a1 \<in> underS r a2" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
764 |
hence a12: "{a1,a2} \<subseteq> under r a2" and "a1 \<noteq> a2" using r.REFL a |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
765 |
unfolding underS_def under_def refl_on_def Field_def by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
766 |
hence "g a1 \<noteq> g a2" using IH1a[OF a2] unfolding inj_on_def by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
767 |
hence "g a1 \<in> underS s (g a2)" using IH1b[OF a2] a12 |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
768 |
unfolding underS_def under_def by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
769 |
} note C = this |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
770 |
have ga: "g a \<in> Field s" unfolding g using s.suc_inField[OF A0 A] . |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
771 |
have aa: "a \<in> under r a" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
772 |
using a r.REFL unfolding under_def underS_def refl_on_def by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
773 |
show ?case proof safe |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
774 |
show "bij_betw g (under r a) (under s (g a))" unfolding bij_betw_def proof safe |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
775 |
show "inj_on g (under r a)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
776 |
by (metis A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
777 |
next |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
778 |
fix a1 assume a1: "a1 \<in> under r a" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
779 |
show "g a1 \<in> under s (g a)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
780 |
by (metis (mono_tags, lifting) B a1 ga mem_Collect_eq s.in_notinI underS_def under_def) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
781 |
next |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
782 |
fix b1 assume b1: "b1 \<in> under s (g a)" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
783 |
show "b1 \<in> g ` under r a" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
784 |
proof(cases "b1 = g a") |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
785 |
case True thus ?thesis using aa by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
786 |
next |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
787 |
case False |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
788 |
show ?thesis |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
789 |
by (metis b1 A IH1a IH1b a bij_betw_def g ga r s s.suc_greater subsetI wellorders_totally_ordered_aux) |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
790 |
qed |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
791 |
qed |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
792 |
next |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
793 |
have "(g a, f a) \<in> s" unfolding g |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
794 |
using \<open>f a \<in> s.AboveS (g ` r.underS a)\<close> s.suc_least_AboveS by blast |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
795 |
thus "g a \<in> under s (f a)" unfolding under_def by auto |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
796 |
qed |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
797 |
qed |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
798 |
} |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
799 |
thus ?thesis unfolding embed_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
800 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
801 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
802 |
corollary ordLeq_def2: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
803 |
"r \<le>o s \<longleftrightarrow> Well_order r \<and> Well_order s \<and> |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
804 |
(\<exists> f. \<forall> a \<in> Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a))" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
805 |
using embed_in_Field[of r s] embed_underS2[of r s] embedI[of r s] |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
806 |
unfolding ordLeq_def by fast |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
807 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
808 |
lemma iso_oproj: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
809 |
assumes r: "Well_order r" and s: "Well_order s" and f: "iso r s f" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
810 |
shows "oproj r s f" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
811 |
using assms unfolding oproj_def |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
812 |
by (metis iso_Field iso_iff3 order_refl) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
813 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
814 |
theorem oproj_embed: |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
815 |
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
816 |
shows "\<exists> g. embed s r g" |
55023
38db7814481d
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
blanchet
parents:
54980
diff
changeset
|
817 |
proof (rule embedI[OF s r, of "inv_into (Field r) f"], unfold underS_def, safe) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
818 |
fix b assume "b \<in> Field s" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
819 |
thus "inv_into (Field r) f b \<in> Field r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
820 |
using oproj_Field2[OF f] by (metis imageI inv_into_into) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
821 |
next |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
822 |
fix a b assume "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
823 |
"inv_into (Field r) f a = inv_into (Field r) f b" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
824 |
with f show False |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
825 |
by (meson FieldI1 in_mono inv_into_injective oproj_def) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
826 |
next |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
827 |
fix a b assume *: "b \<in> Field s" "a \<noteq> b" "(a, b) \<in> s" |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
828 |
{ assume notin: "(inv_into (Field r) f a, inv_into (Field r) f b) \<notin> r" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
829 |
moreover |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
830 |
from *(3) have "a \<in> Field s" unfolding Field_def by auto |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
831 |
then have "(inv_into (Field r) f b, inv_into (Field r) f a) \<in> r" |
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
832 |
by (meson "*"(1) notin f in_mono inv_into_into oproj_def r wo_rel.in_notinI wo_rel.intro) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
833 |
ultimately have "(inv_into (Field r) f b, inv_into (Field r) f a) \<in> r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
834 |
using r by (auto simp: well_order_on_def linear_order_on_def total_on_def) |
63167 | 835 |
with f[unfolded oproj_def compat_def] *(1) \<open>a \<in> Field s\<close> |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
836 |
f_inv_into_f[of b f "Field r"] f_inv_into_f[of a f "Field r"] |
76946
5df58a471d9e
Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk>
parents:
75624
diff
changeset
|
837 |
have "(b, a) \<in> s" by (metis in_mono) |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
838 |
with *(2,3) s have False |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
839 |
by (auto simp: well_order_on_def linear_order_on_def partial_order_on_def antisym_def) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
840 |
} thus "(inv_into (Field r) f a, inv_into (Field r) f b) \<in> r" by blast |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
841 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
842 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
843 |
corollary oproj_ordLeq: |
72126
5de9a5fbf2ec
adjustments for fewer WO assumptions
paulson <lp15@cam.ac.uk>
parents:
70078
diff
changeset
|
844 |
assumes r: "Well_order r" and s: "Well_order s" and f: "oproj r s f" |
5de9a5fbf2ec
adjustments for fewer WO assumptions
paulson <lp15@cam.ac.uk>
parents:
70078
diff
changeset
|
845 |
shows "s \<le>o r" |
5de9a5fbf2ec
adjustments for fewer WO assumptions
paulson <lp15@cam.ac.uk>
parents:
70078
diff
changeset
|
846 |
using oproj_embed[OF assms] r s unfolding ordLeq_def by auto |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54545
diff
changeset
|
847 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
848 |
end |