src/HOL/Cardinals/TODO.txt

moved 'Zorn' into 'Main', since it's a BNF dependency

-1. At the new Isabelle release (after 2009-2), replace the operator List 
from Cardinal_Order_Relation with "lists" from List.thy in standard library. 
A lemma for "lists" is the actual definition of "List".  

0. Add: 

lemma finite_iff_cardOf_nat:
"finite A = ( |A| <o |UNIV :: nat set| )"
using infinite_iff_card_of_nat[of A] 
by (auto simp add: card_of_Well_order ordLess_iff_not_ordLeq)




1. Remember that the version from my computer has a few more theorems than the one 
from the Isabelle site.

2. Many basic cardinal arithmetic facts can be listed as simps!  
The the proofs can be simplified.

3. Add: 

lemma card_of_Plus_ordLeq_infinite:
assumes "infinite C" and "|A| );£o |C|" and "|B| £o |C|"-A
shows "|A <+> B| );£o |C|"-A
proof-
  let ?phi = "(EX a1 a2. a1 ~= a2 );Ù {a1,a2} <= A) Ù -A
              (EX b1 b2. b1 ~= b2 );Ù {b1,b2} <= B)"-A
  show ?thesis
  proof(cases ?phi, auto)
    fix a1 b1 a2 b2 
    assume "a1 );¹ a2" "b1 ¹ b2" "a1 Î A" "a2 Î A" "b1 Î B" "b2 Î B"-A
    hence "|A <+> B| <=o |A <*> B|"
    apply - apply(rule card_of_Plus_Times) by auto
    moreover have "|A <*> B| );£o |C|"-A
    using assms by (auto simp add: card_of_Times_ordLeq_infinite)
    ultimately show ?thesis using ordLeq_transitive by blast
  next
    assume "-=Õa1. a1 );Î A (<_(B (-=Õa2. a1 = a2 );Ú a2 Ï A)"-A
    then obtain a where "A <= {a}" by blast
    {assume "A = {}"
     hence "|A <+> B| =o |B|" 
     using ordIso_symmetric card_of_Plus_empty2 by blast
     hence ?thesis using assms ordIso_ordLeq_trans by blast
    }
    moreover 
    {assume "A = {a}"

    }
  qed
qed


lemma card_of_Plus_ordLess_infinite:
assumes "infinite C" and "|A| <o |C|" and "|B| <o |C|"
shows "|A <+> B| <o |C|"