src/HOL/Cardinals/README.txt
author blanchet
Mon Jan 20 18:24:55 2014 +0100 (2014-01-20)
changeset 55056 b5c94200d081
parent 55027 a74ea6d75571
child 55063 6207fd64519b
permissions -rw-r--r--
renamed '_FP' files to 'BNF_' files
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 well-founded 
blanchet@48975
    20
recursion and well-founded 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 well-order 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 well-order relations,
blanchet@48975
    32
      defines *well-order 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 well-orders.
blanchet@48975
    41
----- 2) Defines the relations "ordLeq", "ordLess" and "ordIso" 
blanchet@48975
    42
      between well-order 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 well-founded.
blanchet@48975
    48
blanchet@48975
    49
-- Cardinal_Order_Relation:
blanchet@48975
    50
---- 1) Defines a *cardinal order* to be a well-order minim w.r.t. "ordLeq" 
blanchet@48975
    51
     (or, equivalently, minimal w.r.t. "ordLess").
blanchet@48975
    52
     ordLess being well-founded together with the well-ordering 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 (order-based) 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@55056
    70
-- BNF_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@55056
    92
1. Most of the definitions and theorems are proved in files prefixed with "BNF_".
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 upper-bound 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 well-order 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 well-order 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 (set-restricted) 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 well-definedness 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 non-parameterized 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@55056
   185
Theory Wellorder_Relation (and BNF_Wellorder_Relation):
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@55056
   194
Theory Wellorder_Embedding (and BNF_Wellorder_Embedding):
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@55056
   204
Theory Constructions_on_Wellorders (and BNF_Constructions_on_Wellorders):
blanchet@48975
   205
- Some of the lemmas in this section are about more general kinds of relations than 
blanchet@48975
   206
  well-orders, 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@55056
   212
Theory Cardinal_Order_Relation (and BNF_Cardinal_Order_Relation):
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?