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?