blanchet@48975

1 
Authors: Andrei Popescu & Dmitriy Traytel

blanchet@48975

2 

blanchet@48975

3 

blanchet@48975

4 
PDF Documentation:

blanchet@48975

5 


blanchet@48975

6 

blanchet@48975

7 
See "document/root.pdf".

blanchet@48975

8 

blanchet@48975

9 

blanchet@48975

10 

blanchet@48975

11 
Short description of the theories' main content:

blanchet@48975

12 


blanchet@48975

13 

blanchet@48975

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

blanchet@48975

15 
extensions of the existing theories Fun, Wellfounded and

blanchet@48975

16 
Order_Relation:

blanchet@48975

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

blanchet@48975

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

blanchet@48975

19 
 Wellfounded_More states variations of wellfounded

blanchet@48975

20 
recursion and wellfounded recursion.

blanchet@48975

21 
 Order_Relation_More fixes a relation, defines upper and lower bounds

blanchet@48975

22 
operators and proves many basic properties for these

blanchet@48975

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

blanchet@48975

24 

blanchet@48975

25 
The "major" theories are:

blanchet@48975

26 
 Wellorder_Relation: Here one fixes a wellorder relation, and then:

blanchet@48975

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

blanchet@48975

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

blanchet@48975

29 
initial segment).

blanchet@48975

30 
 Wellorder_Embedding:

blanchet@48975

31 
 2) For two wellorder relations,

blanchet@48975

32 
defines *wellorder embeddings* as injective functions copying

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

36 
are not, bijections.

blanchet@48975

37 

blanchet@58127

38 
 Wellorder_Constructions:

blanchet@48975

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

blanchet@48975

40 
bounded squares of wellorders.

blanchet@48975

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

blanchet@48975

42 
between wellorder relations (concrete syntax: r <=o r', r <o r' and

blanchet@48975

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

blanchet@48975

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

blanchet@48975

45 
Among the properties proved for these relations:

blanchet@48975

46 
 ordLeq is total;

blanchet@48975

47 
 ordLess (on a fixed type) is wellfounded.

blanchet@48975

48 

blanchet@48975

49 
 Cardinal_Order_Relation:

blanchet@48975

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

blanchet@48975

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

blanchet@48975

52 
ordLess being wellfounded together with the wellordering theorem (from theory Zorn.thy)

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

57 
 3) Proves properties of cardinals, including their

blanchet@48975

58 
interactions with sums, products, unions, lists,

blanchet@48975

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

blanchet@48975

60 
facts concerning the invariance of infinite cardinals

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

64 
 5) Studies the connection between the introduced (orderbased) notion

blanchet@48975

65 
of cardinal and the numeric one previously defined for

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

69 

blanchet@55063

70 
Theory Ordinal_Arithmetic

blanchet@55063

71 

blanchet@55063

72 
Theory Cardinal_Arithmetic (and BNF_Cardinal_Arithmetic)

blanchet@48975

73 

blanchet@48975

74 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

77 
for "working mathematicians":

blanchet@48975

78 
 one_set_greater, one_type_greater (their proofs use the

blanchet@48975

79 
fact that ordinals are totally ordered)

blanchet@48975

80 
 Plus_into_Times, Plus_into_Times_types,

blanchet@48975

81 
Plus_infinite_bij_betw, Plus_infinite_bij_betw_types,

blanchet@48975

82 
Times_same_infinite_bij_betw, Times_same_infinite_bij_betw_types,

blanchet@48975

83 
Times_infinite_bij_betw, Times_infinite_bij_betw_types

blanchet@48975

84 
inj_on_UNION_infinite, List_infinite_bij_betw, List_infinite_bij_betw_types

blanchet@48975

85 
Fpow_infinite_bij_betw

blanchet@48975

86 
(their proofs employ cardinals)

blanchet@48975

87 

blanchet@48975

88 

blanchet@48975

89 

blanchet@48975

90 

blanchet@48975

91 
Minor technicalities and naming issues:

blanchet@48975

92 


blanchet@48975

93 

blanchet@55056

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

blanchet@54481

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

blanchet@54481

96 
desirable.

blanchet@48975

97 

blanchet@48975

98 

blanchet@54481

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

blanchet@54481

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

blanchet@54481

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

blanchet@54481

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

blanchet@54481

103 
segment of a relation.

blanchet@48975

104 

blanchet@48975

105 

blanchet@48975

106 
3. We prefer to define the upperbound operations under, underS,

blanchet@48975

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

blanchet@48975

108 
converse and diagonal, because the former seem more intuitive

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

117 

blanchet@48975

118 

blanchet@48975

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

blanchet@48975

120 
the wellorder relations, we prove the basic results on order relations

blanchet@48975

121 
and bounds as generally as possible.

blanchet@48975

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

blanchet@48975

123 
are stated for wellorder relations, not maximally generally.

blanchet@48975

124 

blanchet@48975

125 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

130 
for most of the tehory.

blanchet@48975

131 

blanchet@48975

132 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

136 

blanchet@48975

137 

blanchet@48975

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

blanchet@48975

139 
bijections, we discovered that a couple of

blanchet@48975

140 
fancier (setrestricted) version of some of them are proved in

blanchet@48975

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

blanchet@48975

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

blanchet@48975

143 
theory for just a couple of minor facts.

blanchet@48975

144 

blanchet@48975

145 

blanchet@48975

146 

blanchet@48975

147 

blanchet@48975

148 

blanchet@48975

149 

blanchet@48975

150 

blanchet@48975

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

blanchet@48975

152 


blanchet@48975

153 

blanchet@55020

154 
Theory Fun_More:

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

159 
 In subsection "Purely functional properties":

blanchet@48975

160 
 Recall lemma "comp_inj_on".

blanchet@48975

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

blanchet@48975

162 
 In subsection "Properties involving Hilbert choice":

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

166 
 A lemma "bij_betw_inv_into_LEFT"  why didn't

blanchet@48975

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

blanchet@48975

168 
 Recall lemma "bij_betw_inv_into".

blanchet@48975

169 
 In subsection "Other facts":

blanchet@48975

170 
 Does the lemma "atLeastLessThan_injective" already exist anywhere?

blanchet@48975

171 

blanchet@55026

172 
Theory Order_Relation_More (and Order_Relation):

blanchet@48975

173 
 In subsection "Auxiliaries":

blanchet@48975

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

blanchet@48975

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

blanchet@48975

176 
This is why "partial_order_def"

blanchet@48975

177 
can afford to use nonparameterized versions of antisym and trans.

blanchet@48975

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

blanchet@48975

179 
 Recall the abbreviations:

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

186 

blanchet@55056

187 
Theory Wellorder_Relation (and BNF_Wellorder_Relation):

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

192 

blanchet@55027

193 
Theory Wellfounded_More:

blanchet@48975

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

blanchet@48975

195 

blanchet@55056

196 
Theory Wellorder_Embedding (and BNF_Wellorder_Embedding):

blanchet@48975

197 
 Recall "inj_on_def" and "bij_betw_def".

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

203 
making impossible to debug theorem instantiations.

blanchet@48975

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

blanchet@48975

205 

blanchet@58127

206 
Theory Wellorder_Constructions (and BNF_Wellorder_Constructions):

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

212 
tends to diverge.

blanchet@48975

213 

blanchet@55056

214 
Theory Cardinal_Order_Relation (and BNF_Cardinal_Order_Relation):

blanchet@48975

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

blanchet@48975

216 
"( A )".

blanchet@48975

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

blanchet@48975

218 
would be a mere instance of card_of_Sigma_mono2.

blanchet@48975

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

blanchet@48975

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

blanchet@48975

221 
also be proved by blast?
