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
```
```     2
```
```     3
```
```     4 PDF Documentation:
```
```     5 -----------------
```
```     6
```
```     7 See "document/root.pdf".
```
```     8
```
```     9
```
```    10
```
```    11 Short description of the theories' main content:
```
```    12 -----------------------------------------------
```
```    13
```
```    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).
```
```    24
```
```    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.
```
```    37
```
```    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.
```
```    48
```
```    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.
```
```    69
```
```    70 Theory Ordinal_Arithmetic
```
```    71
```
```    72 Theory Cardinal_Arithmetic (and BNF_Cardinal_Arithmetic)
```
```    73
```
```    74
```
```    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)
```
```    87
```
```    88
```
```    89
```
```    90
```
```    91 Minor technicalities and naming issues:
```
```    92 ---------------------------------------
```
```    93
```
```    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.
```
```    97
```
```    98
```
```    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.
```
```   104
```
```   105
```
```   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".
```
```   117
```
```   118
```
```   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.
```
```   124
```
```   125
```
```   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.
```
```   131
```
```   132
```
```   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".
```
```   136
```
```   137
```
```   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.
```
```   144
```
```   145
```
```   146
```
```   147
```
```   148
```
```   149
```
```   150
```
```   151 Notes for anyone who would like to enrich these theories in the future
```
```   152 --------------------------------------------------------------------------------------
```
```   153
```
```   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?
```
```   171
```
```   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"
```
```   186
```
```   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"?
```
```   192
```
```   193 Theory Wellfounded_More:
```
```   194   Recall the lemmas "wfrec" and "wf_induct".
```
```   195
```
```   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.
```
```   205
```
```   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.
```
```   213
```
```   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?
```