author | paulson |
Tue, 08 Jan 2002 16:09:09 +0100 | |
changeset 12667 | 7e6eaaa125f2 |
parent 12114 | a8e860c86252 |
child 12776 | 249600a63ba9 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/CardinalArith.thy |
437 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
437 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
Cardinal Arithmetic |
|
7 |
*) |
|
8 |
||
12667 | 9 |
theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite: |
467 | 10 |
|
12667 | 11 |
constdefs |
437 | 12 |
|
12667 | 13 |
InfCard :: "i=>o" |
14 |
"InfCard(i) == Card(i) & nat le i" |
|
437 | 15 |
|
12667 | 16 |
cmult :: "[i,i]=>i" (infixl "|*|" 70) |
17 |
"i |*| j == |i*j|" |
|
18 |
||
19 |
cadd :: "[i,i]=>i" (infixl "|+|" 65) |
|
20 |
"i |+| j == |i+j|" |
|
437 | 21 |
|
12667 | 22 |
csquare_rel :: "i=>i" |
23 |
"csquare_rel(K) == |
|
24 |
rvimage(K*K, |
|
25 |
lam <x,y>:K*K. <x Un y, x, y>, |
|
26 |
rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" |
|
437 | 27 |
|
484 | 28 |
(*This def is more complex than Kunen's but it more easily proved to |
29 |
be a cardinal*) |
|
12667 | 30 |
jump_cardinal :: "i=>i" |
31 |
"jump_cardinal(K) == |
|
1155 | 32 |
UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" |
12667 | 33 |
|
484 | 34 |
(*needed because jump_cardinal(K) might not be the successor of K*) |
12667 | 35 |
csucc :: "i=>i" |
36 |
"csucc(K) == LEAST L. Card(L) & K<L" |
|
484 | 37 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9964
diff
changeset
|
38 |
syntax (xsymbols) |
12667 | 39 |
"op |+|" :: "[i,i] => i" (infixl "\<oplus>" 65) |
40 |
"op |*|" :: "[i,i] => i" (infixl "\<otimes>" 70) |
|
41 |
||
42 |
||
43 |
(*** The following really belong in OrderType ***) |
|
44 |
||
45 |
lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0" |
|
46 |
apply (erule trans_induct3 [of j]) |
|
47 |
apply (simp_all add: oadd_Limit) |
|
48 |
apply (simp add: Union_empty_iff Limit_def lt_def) |
|
49 |
apply blast |
|
50 |
done |
|
51 |
||
52 |
lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j" |
|
53 |
by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff) |
|
54 |
||
55 |
lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j" |
|
56 |
apply (rule lt_trans2) |
|
57 |
apply (erule le_refl) |
|
58 |
apply (simp only: lt_Ord2 oadd_1 [of i, symmetric]) |
|
59 |
apply (blast intro: succ_leI oadd_le_mono) |
|
60 |
done |
|
61 |
||
62 |
lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)" |
|
63 |
apply (simp add: oadd_Limit) |
|
64 |
apply (frule Limit_has_1 [THEN ltD]) |
|
65 |
apply (rule increasing_LimitI) |
|
66 |
apply (rule Ord_0_lt) |
|
67 |
apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) |
|
68 |
apply (force simp add: Union_empty_iff oadd_eq_0_iff |
|
69 |
Limit_is_Ord [of j, THEN Ord_in_Ord]) |
|
70 |
apply auto |
|
71 |
apply (rule_tac x="succ(x)" in bexI) |
|
72 |
apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord]) |
|
73 |
apply (simp add: Limit_def lt_def) |
|
74 |
done |
|
75 |
||
76 |
(*** The following really belong in Cardinal ***) |
|
77 |
||
78 |
lemma lesspoll_not_refl: "~ (i lesspoll i)" |
|
79 |
by (simp add: lesspoll_def) |
|
80 |
||
81 |
lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P" |
|
82 |
by (simp add: lesspoll_def) |
|
83 |
||
84 |
lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))" |
|
85 |
apply (rule CardI) |
|
86 |
apply (simp add: Card_is_Ord) |
|
87 |
apply (clarify dest!: ltD) |
|
88 |
apply (drule bspec, assumption) |
|
89 |
apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) |
|
90 |
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) |
|
91 |
apply (drule lesspoll_trans1, assumption) |
|
92 |
apply (subgoal_tac "B lepoll \<Union>A") |
|
93 |
apply (drule lesspoll_trans1, assumption, blast) |
|
94 |
apply (blast intro: subset_imp_lepoll) |
|
95 |
done |
|
96 |
||
97 |
lemma Card_UN: |
|
98 |
"(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" |
|
99 |
by (blast intro: Card_Union) |
|
100 |
||
101 |
lemma Card_OUN [simp,intro,TC]: |
|
102 |
"(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))" |
|
103 |
by (simp add: OUnion_def Card_0) |
|
9654
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9548
diff
changeset
|
104 |
|
437 | 105 |
end |