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