author | paulson <lp15@cam.ac.uk> |
Mon, 13 May 2024 22:42:40 +0100 | |
changeset 80177 | 1478555580af |
parent 76948 | f33df7529fed |
permissions | -rw-r--r-- |
49310 | 1 |
(* Title: HOL/Cardinals/Wellorder_Relation.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 |
Well-order relations. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
63167 | 8 |
section \<open>Well-Order Relations\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
theory Wellorder_Relation |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
11 |
imports Wellfounded_More |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
51764 | 14 |
context wo_rel |
15 |
begin |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
|
63167 | 17 |
subsection \<open>Auxiliaries\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
|
51764 | 19 |
lemma PREORD: "Preorder r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
20 |
using WELL order_on_defs[of _ r] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
|
51764 | 22 |
lemma PARORD: "Partial_order r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
23 |
using WELL order_on_defs[of _ r] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
|
51764 | 25 |
lemma cases_Total2: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
26 |
"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<Longrightarrow> phi a b); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
((b,a) \<in> r - Id \<Longrightarrow> phi a b); (a = b \<Longrightarrow> phi a b)\<rbrakk> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
\<Longrightarrow> phi a b" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
29 |
using TOTALS by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
|
63167 | 32 |
subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
|
51764 | 34 |
lemma worec_unique_fixpoint: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
35 |
assumes ADM: "adm_wo H" and fp: "f = H f" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
36 |
shows "f = worec H" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
have "adm_wf (r - Id) H" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
39 |
unfolding adm_wf_def |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
40 |
using ADM adm_wo_def[of H] underS_def[of r] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
hence "f = wfrec (r - Id) H" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
42 |
using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
thus ?thesis unfolding worec_def . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
|
63167 | 47 |
subsubsection \<open>Properties of max2\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
|
51764 | 49 |
lemma max2_iff: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
50 |
assumes "a \<in> Field r" and "b \<in> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
51 |
shows "((max2 a b, c) \<in> r) = ((a,c) \<in> r \<and> (b,c) \<in> r)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
proof |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
assume "(max2 a b, c) \<in> r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
thus "(a,c) \<in> r \<and> (b,c) \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
55 |
using assms max2_greater[of a b] TRANS trans_def[of r] by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
assume "(a,c) \<in> r \<and> (b,c) \<in> r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
58 |
thus "(max2 a b, c) \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
59 |
using assms max2_among[of a b] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
|
63167 | 63 |
subsubsection \<open>Properties of minim\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
|
51764 | 65 |
lemma minim_Under: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
66 |
"\<lbrakk>B \<le> Field r; B \<noteq> {}\<rbrakk> \<Longrightarrow> minim B \<in> Under B" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
67 |
by(auto simp add: Under_def minim_inField minim_least) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
|
51764 | 69 |
lemma equals_minim_Under: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
70 |
"\<lbrakk>B \<le> Field r; a \<in> B; a \<in> Under B\<rbrakk> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
\<Longrightarrow> a = minim B" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
72 |
by(auto simp add: Under_def equals_minim) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
|
51764 | 74 |
lemma minim_iff_In_Under: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
75 |
assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
76 |
shows "(a = minim B) = (a \<in> B \<and> a \<in> Under B)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
proof |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
assume "a = minim B" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
thus "a \<in> B \<and> a \<in> Under B" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
80 |
using assms minim_in minim_Under by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
assume "a \<in> B \<and> a \<in> Under B" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
thus "a = minim B" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
84 |
using assms equals_minim_Under by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
|
51764 | 87 |
lemma minim_Under_under: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
88 |
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
89 |
shows "Under A = under (minim A)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
proof- |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
91 |
have "minim A \<in> A" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
92 |
using assms minim_in by auto |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
93 |
then have "Under A \<le> under (minim A)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
94 |
by (simp add: Under_decr under_Under_singl) |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
95 |
moreover have "under (minim A) \<le> Under A" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
96 |
by (meson NE SUB TRANS minim_Under subset_eq under_Under_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
ultimately show ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
|
51764 | 100 |
lemma minim_UnderS_underS: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
101 |
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
102 |
shows "UnderS A = underS (minim A)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
proof- |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
104 |
have "minim A \<in> A" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
105 |
using assms minim_in by auto |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
106 |
then have "UnderS A \<le> underS (minim A)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
107 |
by (simp add: UnderS_decr underS_UnderS_singl) |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
108 |
moreover have "underS (minim A) \<le> UnderS A" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
109 |
by (meson ANTISYM NE SUB TRANS minim_Under subset_eq underS_Under_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
ultimately show ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
qed |
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 |
|
63167 | 114 |
subsubsection \<open>Properties of supr\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
115 |
|
51764 | 116 |
lemma supr_Above: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
117 |
assumes "Above B \<noteq> {}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
118 |
shows "supr B \<in> Above B" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
119 |
by (simp add: assms Above_Field minim_in supr_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
|
51764 | 121 |
lemma supr_greater: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
122 |
assumes "Above B \<noteq> {}" "b \<in> B" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
123 |
shows "(b, supr B) \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
124 |
using assms Above_def supr_Above by fastforce |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
125 |
|
51764 | 126 |
lemma supr_least_Above: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
127 |
assumes "a \<in> Above B" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
128 |
shows "(supr B, a) \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
129 |
by (simp add: assms Above_Field minim_least supr_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
|
51764 | 131 |
lemma supr_least: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
132 |
"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r)\<rbrakk> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
\<Longrightarrow> (supr B, a) \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
134 |
by(auto simp add: supr_least_Above Above_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
|
51764 | 136 |
lemma equals_supr_Above: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
137 |
assumes "a \<in> Above B" "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
138 |
shows "a = supr B" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
139 |
by (simp add: assms Above_Field equals_minim supr_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
140 |
|
51764 | 141 |
lemma equals_supr: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
142 |
assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
143 |
ABV: "\<And> b. b \<in> B \<Longrightarrow> (b,a) \<in> r" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
144 |
MINIM: "\<And> a'. \<lbrakk> a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
145 |
shows "a = supr B" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
have "a \<in> Above B" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
148 |
unfolding Above_def using ABV IN by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
have "\<And> a'. a' \<in> Above B \<Longrightarrow> (a,a') \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
151 |
unfolding Above_def using MINIM by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
ultimately show ?thesis |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
153 |
using equals_supr_Above SUB by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
155 |
|
51764 | 156 |
lemma supr_inField: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
157 |
assumes "Above B \<noteq> {}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
158 |
shows "supr B \<in> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
159 |
by (simp add: Above_Field assms minim_inField supr_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
160 |
|
51764 | 161 |
lemma supr_above_Above: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
162 |
assumes SUB: "B \<le> Field r" and ABOVE: "Above B \<noteq> {}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
163 |
shows "Above B = above (supr B)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
164 |
apply (clarsimp simp: Above_def above_def set_eq_iff) |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
165 |
by (meson ABOVE FieldI2 SUB TRANS supr_greater supr_least transD) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
|
51764 | 167 |
lemma supr_under: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
168 |
assumes "a \<in> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
169 |
shows "a = supr (under a)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
171 |
have "under a \<le> Field r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
172 |
using under_Field[of r] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
173 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
have "under a \<noteq> {}" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
175 |
using assms Refl_under_in[of r] REFL by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
177 |
have "a \<in> Above (under a)" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
178 |
using in_Above_under[of _ r] assms by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
have "\<forall>a' \<in> Above (under a). (a,a') \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
181 |
by (auto simp: Above_def above_def REFL Refl_under_in assms) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
ultimately show ?thesis |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
183 |
using equals_supr_Above by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
184 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
|
63167 | 187 |
subsubsection \<open>Properties of successor\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
|
51764 | 189 |
lemma suc_least: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
190 |
"\<lbrakk>B \<le> Field r; a \<in> Field r; (\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r)\<rbrakk> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
\<Longrightarrow> (suc B, a) \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
192 |
by(auto simp add: suc_least_AboveS AboveS_def) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
|
51764 | 194 |
lemma equals_suc: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
195 |
assumes SUB: "B \<le> Field r" and IN: "a \<in> Field r" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
196 |
ABVS: "\<And> b. b \<in> B \<Longrightarrow> a \<noteq> b \<and> (b,a) \<in> r" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
197 |
MINIM: "\<And> a'. \<lbrakk>a' \<in> Field r; \<And> b. b \<in> B \<Longrightarrow> a' \<noteq> b \<and> (b,a') \<in> r\<rbrakk> \<Longrightarrow> (a,a') \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
198 |
shows "a = suc B" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
199 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
200 |
have "a \<in> AboveS B" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
201 |
unfolding AboveS_def using ABVS IN by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
203 |
have "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
204 |
unfolding AboveS_def using MINIM by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
ultimately show ?thesis |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
206 |
using equals_suc_AboveS SUB by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
|
51764 | 209 |
lemma suc_above_AboveS: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
210 |
assumes SUB: "B \<le> Field r" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
211 |
ABOVE: "AboveS B \<noteq> {}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
212 |
shows "AboveS B = above (suc B)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
213 |
using assms |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
proof(unfold AboveS_def above_def, auto) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
fix a assume "a \<in> Field r" "\<forall>b \<in> B. a \<noteq> b \<and> (b,a) \<in> r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
with suc_least assms |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
show "(suc B,a) \<in> r" by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
fix b assume "(suc B, b) \<in> r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
thus "b \<in> Field r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
221 |
using REFL refl_on_def[of _ r] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
fix a b |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
225 |
with assms suc_greater[of B a] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
have "(a,suc B) \<in> r" by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
227 |
thus "(a,b) \<in> r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
228 |
using 1 TRANS trans_def[of r] by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
fix a |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
231 |
assume "(suc B, a) \<in> r" and 2: "a \<in> B" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
232 |
thus False |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
233 |
by (metis ABOVE ANTISYM SUB antisymD suc_greater) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
|
51764 | 236 |
lemma suc_singl_pred: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
237 |
assumes IN: "a \<in> Field r" and ABOVE_NE: "aboveS a \<noteq> {}" and |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
238 |
REL: "(a',suc {a}) \<in> r" and DIFF: "a' \<noteq> suc {a}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
239 |
shows "a' = a \<or> (a',a) \<in> r" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
240 |
proof- |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
241 |
have *: "suc {a} \<in> Field r \<and> a' \<in> Field r" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
242 |
using WELL REL well_order_on_domain by metis |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
243 |
{assume **: "a' \<noteq> a" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
244 |
hence "(a,a') \<in> r \<or> (a',a) \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
245 |
using TOTAL IN * by (auto simp add: total_on_def) |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
246 |
moreover |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
247 |
{assume "(a,a') \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
248 |
with ** * assms WELL suc_least[of "{a}" a'] |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
249 |
have "(suc {a},a') \<in> r" by auto |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
250 |
with REL DIFF * ANTISYM antisym_def[of r] |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
251 |
have False by simp |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
252 |
} |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
253 |
ultimately have "(a',a) \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
254 |
by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
255 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
256 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
257 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
258 |
|
51764 | 259 |
lemma under_underS_suc: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
260 |
assumes IN: "a \<in> Field r" and ABV: "aboveS a \<noteq> {}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
261 |
shows "underS (suc {a}) = under a" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
262 |
proof - |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
263 |
have "AboveS {a} \<noteq> {}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
264 |
using ABV aboveS_AboveS_singl[of r] by auto |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
265 |
then have 2: "a \<noteq> suc {a} \<and> (a,suc {a}) \<in> r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
266 |
using suc_greater[of "{a}" a] IN by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
have "underS (suc {a}) \<le> under a" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
268 |
using ABV IN REFL Refl_under_in underS_E under_def wo_rel.suc_singl_pred wo_rel_axioms by fastforce |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
moreover |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
have "under a \<le> underS (suc {a})" |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
271 |
by (simp add: "2" ANTISYM TRANS subsetI underS_I under_underS_trans) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
ultimately show ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
273 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
274 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
275 |
|
63167 | 276 |
subsubsection \<open>Properties of order filters\<close> |
54477 | 277 |
|
278 |
lemma ofilter_Under[simp]: |
|
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
279 |
assumes "A \<le> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
280 |
shows "ofilter(Under A)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
281 |
by (clarsimp simp: ofilter_def) (meson TRANS Under_Field subset_eq under_Under_trans) |
54477 | 282 |
|
283 |
lemma ofilter_UnderS[simp]: |
|
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
284 |
assumes "A \<le> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
285 |
shows "ofilter(UnderS A)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
286 |
by (clarsimp simp: ofilter_def) (meson ANTISYM TRANS UnderS_Field subset_eq under_UnderS_trans) |
54477 | 287 |
|
288 |
lemma ofilter_Int[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A Int B)" |
|
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
289 |
unfolding ofilter_def by blast |
54477 | 290 |
|
291 |
lemma ofilter_Un[simp]: "\<lbrakk>ofilter A; ofilter B\<rbrakk> \<Longrightarrow> ofilter(A \<union> B)" |
|
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
292 |
unfolding ofilter_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
293 |
|
51764 | 294 |
lemma ofilter_INTER: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
295 |
"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
296 |
unfolding ofilter_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
297 |
|
51764 | 298 |
lemma ofilter_Inter: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
299 |
"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
300 |
unfolding ofilter_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
301 |
|
51764 | 302 |
lemma ofilter_Union: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
303 |
"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
304 |
unfolding ofilter_def by blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
305 |
|
51764 | 306 |
lemma ofilter_under_Union: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
307 |
"ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
308 |
using ofilter_under_UNION [of A] by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
309 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
310 |
|
63167 | 311 |
subsubsection \<open>Other properties\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
|
51764 | 313 |
lemma Trans_Under_regressive: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
314 |
assumes NE: "A \<noteq> {}" and SUB: "A \<le> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
315 |
shows "Under(Under A) \<le> Under A" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
316 |
by (metis INT_E NE REFL Refl_under_Under SUB empty_iff minim_Under minim_Under_under subsetI) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
317 |
|
51764 | 318 |
lemma ofilter_suc_Field: |
76948
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
319 |
assumes OF: "ofilter A" and NE: "A \<noteq> Field r" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
320 |
shows "ofilter (A \<union> {suc A})" |
f33df7529fed
Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk>
parents:
68652
diff
changeset
|
321 |
by (metis NE OF REFL Refl_under_underS ofilter_underS_Field suc_underS under_ofilter) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
322 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
323 |
(* FIXME: needed? *) |
51764 | 324 |
declare |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
325 |
minim_in[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
326 |
minim_inField[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
327 |
minim_least[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
328 |
under_ofilter[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
329 |
underS_ofilter[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
330 |
Field_ofilter[simp] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
331 |
|
51764 | 332 |
end |
333 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
334 |
abbreviation "worec \<equiv> wo_rel.worec" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
335 |
abbreviation "adm_wo \<equiv> wo_rel.adm_wo" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
336 |
abbreviation "isMinim \<equiv> wo_rel.isMinim" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
337 |
abbreviation "minim \<equiv> wo_rel.minim" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
338 |
abbreviation "max2 \<equiv> wo_rel.max2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
339 |
abbreviation "supr \<equiv> wo_rel.supr" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
340 |
abbreviation "suc \<equiv> wo_rel.suc" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
341 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
342 |
end |