src/ZF/CardinalArith.thy
changeset 12667 7e6eaaa125f2
parent 12114 a8e860c86252
child 12776 249600a63ba9
     1.1 --- a/src/ZF/CardinalArith.thy	Tue Jan 08 15:39:47 2002 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Tue Jan 08 16:09:09 2002 +0100
     1.3 @@ -6,41 +6,100 @@
     1.4  Cardinal Arithmetic
     1.5  *)
     1.6  
     1.7 -CardinalArith = Cardinal + OrderArith + ArithSimp + Finite + 
     1.8 -consts
     1.9 +theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
    1.10  
    1.11 -  InfCard       :: i=>o
    1.12 -  "|*|"         :: [i,i]=>i       (infixl 70)
    1.13 -  "|+|"         :: [i,i]=>i       (infixl 65)
    1.14 -  csquare_rel   :: i=>i
    1.15 -  jump_cardinal :: i=>i
    1.16 -  csucc         :: i=>i
    1.17 +constdefs
    1.18  
    1.19 -defs
    1.20 +  InfCard       :: "i=>o"
    1.21 +    "InfCard(i) == Card(i) & nat le i"
    1.22  
    1.23 -  InfCard_def  "InfCard(i) == Card(i) & nat le i"
    1.24 -
    1.25 -  cadd_def     "i |+| j == |i+j|"
    1.26 -
    1.27 -  cmult_def    "i |*| j == |i*j|"
    1.28 +  cmult         :: "[i,i]=>i"       (infixl "|*|" 70)
    1.29 +    "i |*| j == |i*j|"
    1.30 +  
    1.31 +  cadd          :: "[i,i]=>i"       (infixl "|+|" 65)
    1.32 +    "i |+| j == |i+j|"
    1.33  
    1.34 -  csquare_rel_def
    1.35 -  "csquare_rel(K) ==   
    1.36 -        rvimage(K*K,   
    1.37 -                lam <x,y>:K*K. <x Un y, x, y>, 
    1.38 -                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    1.39 +  csquare_rel   :: "i=>i"
    1.40 +    "csquare_rel(K) ==   
    1.41 +	  rvimage(K*K,   
    1.42 +		  lam <x,y>:K*K. <x Un y, x, y>, 
    1.43 +		  rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    1.44  
    1.45    (*This def is more complex than Kunen's but it more easily proved to
    1.46      be a cardinal*)
    1.47 -  jump_cardinal_def
    1.48 -      "jump_cardinal(K) ==   
    1.49 +  jump_cardinal :: "i=>i"
    1.50 +    "jump_cardinal(K) ==   
    1.51           UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
    1.52 -
    1.53 +  
    1.54    (*needed because jump_cardinal(K) might not be the successor of K*)
    1.55 -  csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
    1.56 +  csucc         :: "i=>i"
    1.57 +    "csucc(K) == LEAST L. Card(L) & K<L"
    1.58  
    1.59  syntax (xsymbols)
    1.60 -  "op |+|"     :: [i,i] => i          (infixl "\\<oplus>" 65)
    1.61 -  "op |*|"     :: [i,i] => i          (infixl "\\<otimes>" 70)
    1.62 +  "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
    1.63 +  "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
    1.64 +
    1.65 +
    1.66 +(*** The following really belong in OrderType ***)
    1.67 +
    1.68 +lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
    1.69 +apply (erule trans_induct3 [of j])
    1.70 +apply (simp_all add: oadd_Limit)
    1.71 +apply (simp add: Union_empty_iff Limit_def lt_def)
    1.72 +apply blast
    1.73 +done
    1.74 +
    1.75 +lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
    1.76 +by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
    1.77 +
    1.78 +lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
    1.79 +apply (rule lt_trans2) 
    1.80 +apply (erule le_refl) 
    1.81 +apply (simp only: lt_Ord2  oadd_1 [of i, symmetric]) 
    1.82 +apply (blast intro: succ_leI oadd_le_mono)
    1.83 +done
    1.84 +
    1.85 +lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)"
    1.86 +apply (simp add: oadd_Limit)
    1.87 +apply (frule Limit_has_1 [THEN ltD])
    1.88 +apply (rule increasing_LimitI)
    1.89 + apply (rule Ord_0_lt)
    1.90 +  apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
    1.91 + apply (force simp add: Union_empty_iff oadd_eq_0_iff
    1.92 +                        Limit_is_Ord [of j, THEN Ord_in_Ord])
    1.93 +apply auto
    1.94 +apply (rule_tac x="succ(x)" in bexI)
    1.95 + apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
    1.96 +apply (simp add: Limit_def lt_def) 
    1.97 +done
    1.98 +
    1.99 +(*** The following really belong in Cardinal ***)
   1.100 +
   1.101 +lemma lesspoll_not_refl: "~ (i lesspoll i)"
   1.102 +by (simp add: lesspoll_def) 
   1.103 +
   1.104 +lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P"
   1.105 +by (simp add: lesspoll_def) 
   1.106 +
   1.107 +lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
   1.108 +apply (rule CardI) 
   1.109 + apply (simp add: Card_is_Ord) 
   1.110 +apply (clarify dest!: ltD)
   1.111 +apply (drule bspec, assumption) 
   1.112 +apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 
   1.113 +apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
   1.114 +apply (drule lesspoll_trans1, assumption) 
   1.115 +apply (subgoal_tac "B lepoll \<Union>A")
   1.116 + apply (drule lesspoll_trans1, assumption, blast) 
   1.117 +apply (blast intro: subset_imp_lepoll) 
   1.118 +done
   1.119 +
   1.120 +lemma Card_UN:
   1.121 +     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 
   1.122 +by (blast intro: Card_Union) 
   1.123 +
   1.124 +lemma Card_OUN [simp,intro,TC]:
   1.125 +     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
   1.126 +by (simp add: OUnion_def Card_0) 
   1.127  
   1.128  end