summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Cardinals/README.txt

author | wenzelm |

Fri Oct 27 13:50:08 2017 +0200 (23 months ago) | |

changeset 66924 | b4d4027f743b |

parent 58127 | b7cab82f488e |

permissions | -rw-r--r-- |

more permissive;

1 Authors: Andrei Popescu & Dmitriy Traytel

4 PDF Documentation:

5 -----------------

7 See "document/root.pdf".

11 Short description of the theories' main content:

12 -----------------------------------------------

14 The "minor" theories Fun_More, Wellfounded_More and Order_Relation_More are

15 extensions of the existing theories Fun, Wellfounded and

16 Order_Relation:

17 -- Fun_More states more facts (mainly) concerning injections, bijections,

18 inverses, and (numeric) cardinals of finite sets.

19 -- Wellfounded_More states variations of well-founded

20 recursion and well-founded recursion.

21 -- Order_Relation_More fixes a relation, defines upper and lower bounds

22 operators and proves many basic properties for these

23 (depending on assumptions such as reflexivity or transitivity).

25 The "major" theories are:

26 -- Wellorder_Relation: Here one fixes a well-order relation, and then:

27 ----- 1) Defines the concepts of maximum (of two elements), minimum (of a set), supremum,

28 successor (of a set), and order filter (i.e., downwards closed set, a.k.a.

29 initial segment).

30 -- Wellorder_Embedding:

31 ----- 2) For two well-order relations,

32 defines *well-order embeddings* as injective functions copying

33 the source into an order filter of the target and *compatible functions*

34 as those preserving the order. Also, *isomorphisms*

35 and *strict embeddings* are defined to be embeddings that are, and respectively

36 are not, bijections.

38 -- Wellorder_Constructions:

39 ----- 1) Defines direct images, restrictions, disjoint unions and

40 bounded squares of well-orders.

41 ----- 2) Defines the relations "ordLeq", "ordLess" and "ordIso"

42 between well-order relations (concrete syntax: r <=o r', r <o r' and

43 r =o r', respectively), defined by the existence of an embedding,

44 strict embedding and isomorphism, respectively between the two members.

45 Among the properties proved for these relations:

46 --------- ordLeq is total;

47 --------- ordLess (on a fixed type) is well-founded.

49 -- Cardinal_Order_Relation:

50 ---- 1) Defines a *cardinal order* to be a well-order minim w.r.t. "ordLeq"

51 (or, equivalently, minimal w.r.t. "ordLess").

52 ordLess being well-founded together with the well-ordering theorem (from theory Zorn.thy)

53 ensures the existence of a cardinal relation on any given set. In addition,

54 a cardinal relation on a set is unique up to order isomorphism.

55 ---- 2) Defines the cardinal of a set A, |A|, to be SOME cardinal

56 order on it (unique up to =o, according to the above).

57 ---- 3) Proves properties of cardinals, including their

58 interactions with sums, products, unions, lists,

59 powersets, sets of finite sets. Among them, nontrivial

60 facts concerning the invariance of infinite cardinals

61 under some of these constructs -- e.g., if A is infinite,

62 than the cardinal of lists/words over A is the same (up to

63 the "cardinal equality" =o) as that of A.

64 ---- 5) Studies the connection between the introduced (order-based) notion

65 of cardinal and the numeric one previously defined for

66 finite sets (operator "card"). On the way, one introduces the cardinal omega

67 (natLeq) and the finite cardinals (natLeq_on n).

68 ---- 6) Defines and proves the existence of successor cardinals.

70 Theory Ordinal_Arithmetic

72 Theory Cardinal_Arithmetic (and BNF_Cardinal_Arithmetic)

75 Here is a list of names of proved facts concerning cardinalities that are

76 expressed independently of notions of order, and of potential interest

77 for "working mathematicians":

78 --- one_set_greater, one_type_greater (their proofs use the

79 fact that ordinals are totally ordered)

80 --- Plus_into_Times, Plus_into_Times_types,

81 Plus_infinite_bij_betw, Plus_infinite_bij_betw_types,

82 Times_same_infinite_bij_betw, Times_same_infinite_bij_betw_types,

83 Times_infinite_bij_betw, Times_infinite_bij_betw_types

84 inj_on_UNION_infinite, List_infinite_bij_betw, List_infinite_bij_betw_types

85 Fpow_infinite_bij_betw

86 (their proofs employ cardinals)

91 Minor technicalities and naming issues:

92 ---------------------------------------

94 1. Most of the definitions and theorems are proved in files prefixed with "BNF_".

95 Bootstrapping considerations (for the (co)datatype package) made this division

96 desirable.

99 2. Even though we would have preferred to use "initial segment" instead of

100 "order filter", we chose the latter to avoid terminological clash with the

101 operator "init_seg_of" from Zorn.thy. The latter expresses a related, but

102 different concept -- it considers a relation, rather than a set, as initial

103 segment of a relation.

106 3. We prefer to define the upper-bound operations under, underS,

107 etc., as opposed to working with combinations of relation image,

108 converse and diagonal, because the former seem more intuitive

109 notations when we think of orderings (but of course we cannot

110 define them as abbreviations, as this would have a global

111 effect, also affecting cases where one does not think of relations

112 as orders). Moreover, in my locales the relation parameter r for

113 under, underS etc. is fixed, hence these operations can keep r

114 implicit. To get a concrete glimpse at my aesthetic reason for

115 introducing these operations: otherwise, instead of "underS a",

116 we would have to write "(r - Id)^-1 `` {a}" or "r^-1 `` {a} - Id".

119 4. Even though the main focus of this development are

120 the well-order relations, we prove the basic results on order relations

121 and bounds as generally as possible.

122 To the contrary, the results concerning minima, suprema and successors

123 are stated for well-order relations, not maximally generally.

126 5. "Refl_on A r" requires in particular that "r <= A <*> A",

127 and therefore whenever "Refl_on A r", we have that necessarily

128 "A = Field r". This means that in a theory of orders the domain

129 A would be redundant -- we decided not to include it explicitly

130 for most of the tehory.

133 6. An infinite ordinal/cardinal is one for which the field is infinite.

134 We always prefer the slightly more verbose "finite (Field r)" to the more

135 compact but less standard equivalent condition "finite r".

138 7. After we proved lots of facts about injections and

139 bijections, we discovered that a couple of

140 fancier (set-restricted) version of some of them are proved in

141 the theory FuncSet. However, we did not need here restricted

142 abstraction and such, and felt we should not import the whole

143 theory for just a couple of minor facts.

151 Notes for anyone who would like to enrich these theories in the future

152 --------------------------------------------------------------------------------------

154 Theory Fun_More:

155 - Careful: "inj" is an abbreviation for "inj_on UNIV", while

156 "bij" is not an abreviation for "bij_betw UNIV UNIV", but

157 a defined constant; there is no "surj_betw", but only "surj".

158 "inv" is an abbreviation for "inv_into UNIV"

159 - In subsection "Purely functional properties":

160 -- Recall lemma "comp_inj_on".

161 -- A lemma for inj_on corresponding to "bij_betw_same_card" already exists, and is called "card_inj_on_le".

162 - In subsection "Properties involving Hilbert choice":

163 -- One should refrain from trying to prove "intuitive" properties of f conditioned

164 by properties of (inv_into f A), such as "bij_betw A' A (inv_into f A) ==> bij_betw A A' f".

165 They usually do not hold, since one cannot usually infer the well-definedness of "inv_into f A".

166 - A lemma "bij_betw_inv_into_LEFT" -- why didn't

167 "proof(auto simp add: bij_betw_inv_into_left)" finish the proof?

168 -- Recall lemma "bij_betw_inv_into".

169 - In subsection "Other facts":

170 -- Does the lemma "atLeastLessThan_injective" already exist anywhere?

172 Theory Order_Relation_More (and Order_Relation):

173 - In subsection "Auxiliaries":

174 -- Recall the lemmas "order_on_defs", "Field_def", "Domain_def", "Range_def", "converse_def".

175 -- Recall that "refl_on r A" forces r to not be defined outside A.

176 This is why "partial_order_def"

177 can afford to use non-parameterized versions of antisym and trans.

178 -- Recall the ASCII notation for "converse r": "r ^-1".

179 -- Recall the abbreviations:

180 abbreviation "Refl r ≡ refl_on (Field r) r"

181 abbreviation "Preorder r ≡ preorder_on (Field r) r"

182 abbreviation "Partial_order r ≡ partial_order_on (Field r) r"

183 abbreviation "Total r ≡ total_on (Field r) r"

184 abbreviation "Linear_order r ≡ linear_order_on (Field r) r"

185 abbreviation "Well_order r ≡ well_order_on (Field r) r"

187 Theory Wellorder_Relation (and BNF_Wellorder_Relation):

188 - In subsection "Auxiliaries": recall lemmas "order_on_defs"

189 - In subsection "The notions of maximum, minimum, supremum, successor and order filter":

190 Should we define all constants from "wo_rel" in "rel" instead,

191 so that their outside definition not be conditional in "wo_rel r"?

193 Theory Wellfounded_More:

194 Recall the lemmas "wfrec" and "wf_induct".

196 Theory Wellorder_Embedding (and BNF_Wellorder_Embedding):

197 - Recall "inj_on_def" and "bij_betw_def".

198 - Line 5 in the proof of lemma embed_in_Field: we have to figure out for this and many other

199 situations: Why did it work without annotations to Refl_under_in?

200 - At the proof of theorem "wellorders_totally_ordered" (and, similarly, elsewhere):

201 Had we used metavariables instead of local definitions for H, f, g and test, the

202 goals (in the goal window) would have become unreadable,

203 making impossible to debug theorem instantiations.

204 - At lemma "embed_unique": If we add the attribute "rule format" at lemma, we get an error at qed.

206 Theory Wellorder_Constructions (and BNF_Wellorder_Constructions):

207 - Some of the lemmas in this section are about more general kinds of relations than

208 well-orders, but it is not clear whether they are useful in such more general contexts.

209 - Recall that "equiv" does not have the "equiv_on" and "Equiv" versions,

210 like the order relation. "equiv" corresponds, for instance, to "well_order_on".

211 - The lemmas "ord_trans" are not clearly useful together, as their employment within blast or auto

212 tends to diverge.

214 Theory Cardinal_Order_Relation (and BNF_Cardinal_Order_Relation):

215 - Careful: if "|..|" meets an outer parehthesis, an extra space needs to be inserted, as in

216 "( |A| )".

217 - At lemma like ordLeq_Sigma_mono1: Not worth stating something like ordLeq_Sigma_mono2 --

218 would be a mere instance of card_of_Sigma_mono2.

219 - At lemma ordLeq_Sigma_cong2: Again, no reason for stating something like ordLeq_Sigma_cong2.

220 - At lemma Fpow_Pow_finite: why wouldn't a version of this lemma with "... Int finite"

221 also be proved by blast?