src/HOL/Cardinals/TODO.txt
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 49310 6e30078de4f0
permissions -rw-r--r--
tuned;
     1 -1. At the new Isabelle release (after 2009-2), replace the operator List 
     2 from Cardinal_Order_Relation with "lists" from List.thy in standard library. 
     3 A lemma for "lists" is the actual definition of "List".  
     4 
     5 0. Add: 
     6 
     7 lemma finite_iff_cardOf_nat:
     8 "finite A = ( |A| <o |UNIV :: nat set| )"
     9 using infinite_iff_card_of_nat[of A] 
    10 by (auto simp add: card_of_Well_order ordLess_iff_not_ordLeq)
    11 
    12 
    13 
    14 
    15 1. Remember that the version from my computer has a few more theorems than the one 
    16 from the Isabelle site.
    17 
    18 2. Many basic cardinal arithmetic facts can be listed as simps!  
    19 The the proofs can be simplified.
    20 
    21 3. Add: 
    22 
    23 lemma card_of_Plus_ordLeq_infinite:
    24 assumes "infinite C" and "|A| );o |C|" and "|B| o |C|"-A
    25 shows "|A <+> B| );o |C|"-A
    26 proof-
    27   let ?phi = "(EX a1 a2. a1 ~= a2 ); {a1,a2} <= A)  -A
    28               (EX b1 b2. b1 ~= b2 ); {b1,b2} <= B)"-A
    29   show ?thesis
    30   proof(cases ?phi, auto)
    31     fix a1 b1 a2 b2 
    32     assume "a1 ); a2" "b1  b2" "a1  A" "a2  A" "b1  B" "b2  B"-A
    33     hence "|A <+> B| <=o |A <*> B|"
    34     apply - apply(rule card_of_Plus_Times) by auto
    35     moreover have "|A <*> B| );o |C|"-A
    36     using assms by (auto simp add: card_of_Times_ordLeq_infinite)
    37     ultimately show ?thesis using ordLeq_transitive by blast
    38   next
    39     assume "-=a1. a1 ); A (<_(B (-=a2. a1 = a2 ); a2  A)"-A
    40     then obtain a where "A <= {a}" by blast
    41     {assume "A = {}"
    42      hence "|A <+> B| =o |B|" 
    43      using ordIso_symmetric card_of_Plus_empty2 by blast
    44      hence ?thesis using assms ordIso_ordLeq_trans by blast
    45     }
    46     moreover 
    47     {assume "A = {a}"
    48 
    49     }
    50   qed
    51 qed
    52 
    53 
    54 lemma card_of_Plus_ordLess_infinite:
    55 assumes "infinite C" and "|A| <o |C|" and "|B| <o |C|"
    56 shows "|A <+> B| <o |C|"
    57 
    58 
    59