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@48975

38 
 Constructions_on_Wellorders:

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@48975

70 
 Cardinal_Arithmetic

blanchet@48975

71 

blanchet@48975

72 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

75 
for "working mathematicians":

blanchet@48975

76 
 one_set_greater, one_type_greater (their proofs use the

blanchet@48975

77 
fact that ordinals are totally ordered)

blanchet@48975

78 
 Plus_into_Times, Plus_into_Times_types,

blanchet@48975

79 
Plus_infinite_bij_betw, Plus_infinite_bij_betw_types,

blanchet@48975

80 
Times_same_infinite_bij_betw, Times_same_infinite_bij_betw_types,

blanchet@48975

81 
Times_infinite_bij_betw, Times_infinite_bij_betw_types

blanchet@48975

82 
inj_on_UNION_infinite, List_infinite_bij_betw, List_infinite_bij_betw_types

blanchet@48975

83 
Fpow_infinite_bij_betw

blanchet@48975

84 
(their proofs employ cardinals)

blanchet@48975

85 

blanchet@48975

86 

blanchet@48975

87 

blanchet@48975

88 

blanchet@48975

89 
Minor technicalities and naming issues:

blanchet@48975

90 


blanchet@48975

91 

blanchet@54481

92 
1. Most of the definitions and theorems are proved in files suffixed with "_FP".

blanchet@54481

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

blanchet@54481

94 
desirable.

blanchet@48975

95 

blanchet@48975

96 

blanchet@54481

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

blanchet@54481

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

blanchet@54481

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

blanchet@54481

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

blanchet@54481

101 
segment of a relation.

blanchet@48975

102 

blanchet@48975

103 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

106 
converse and diagonal, because the former seem more intuitive

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

115 

blanchet@48975

116 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

119 
and bounds as generally as possible.

blanchet@48975

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

blanchet@48975

121 
are stated for wellorder relations, not maximally generally.

blanchet@48975

122 

blanchet@48975

123 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

128 
for most of the tehory.

blanchet@48975

129 

blanchet@48975

130 

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

134 

blanchet@48975

135 

blanchet@48975

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

blanchet@48975

137 
bijections, we discovered that a couple of

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

141 
theory for just a couple of minor facts.

blanchet@48975

142 

blanchet@48975

143 

blanchet@48975

144 

blanchet@48975

145 

blanchet@48975

146 

blanchet@48975

147 

blanchet@48975

148 

blanchet@48975

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

blanchet@48975

150 


blanchet@48975

151 

blanchet@55020

152 
Theory Fun_More:

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

157 
 In subsection "Purely functional properties":

blanchet@48975

158 
 Recall lemma "comp_inj_on".

blanchet@48975

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

blanchet@48975

160 
 In subsection "Properties involving Hilbert choice":

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

164 
 A lemma "bij_betw_inv_into_LEFT"  why didn't

blanchet@48975

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

blanchet@48975

166 
 Recall lemma "bij_betw_inv_into".

blanchet@48975

167 
 In subsection "Other facts":

blanchet@48975

168 
 Does the lemma "atLeastLessThan_injective" already exist anywhere?

blanchet@48975

169 

blanchet@55026

170 
Theory Order_Relation_More (and Order_Relation):

blanchet@48975

171 
 In subsection "Auxiliaries":

blanchet@48975

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

blanchet@48975

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

blanchet@48975

174 
This is why "partial_order_def"

blanchet@48975

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

blanchet@48975

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

blanchet@48975

177 
 Recall the abbreviations:

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

184 

blanchet@54481

185 
Theory Wellorder_Relation (and Wellorder_Relation_FP):

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

190 

blanchet@55027

191 
Theory Wellfounded_More:

blanchet@48975

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

blanchet@48975

193 

blanchet@54481

194 
Theory Wellorder_Embedding (and Wellorder_Embedding_FP):

blanchet@48975

195 
 Recall "inj_on_def" and "bij_betw_def".

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

201 
making impossible to debug theorem instantiations.

blanchet@48975

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

blanchet@48975

203 

blanchet@54481

204 
Theory Constructions_on_Wellorders (and Constructions_on_Wellorders_FP):

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

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

blanchet@48975

210 
tends to diverge.

blanchet@48975

211 

blanchet@54481

212 
Theory Cardinal_Order_Relation (and Cardinal_Order_Relation_FP):

blanchet@48975

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

blanchet@48975

214 
"( A )".

blanchet@48975

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

blanchet@48975

216 
would be a mere instance of card_of_Sigma_mono2.

blanchet@48975

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

blanchet@48975

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

blanchet@48975

219 
also be proved by blast?
