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 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? ```