src/ZF/CardinalArith.thy
author paulson
Wed Jan 16 17:52:06 2002 +0100 (2002-01-16)
changeset 12776 249600a63ba9
parent 12667 7e6eaaa125f2
child 12820 02e2ff3e4d37
permissions -rw-r--r--
Isar version of AC
clasohm@1478
     1
(*  Title:      ZF/CardinalArith.thy
lcp@437
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@437
     4
    Copyright   1994  University of Cambridge
lcp@437
     5
lcp@437
     6
Cardinal Arithmetic
lcp@437
     7
*)
lcp@437
     8
paulson@12667
     9
theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
lcp@467
    10
paulson@12667
    11
constdefs
lcp@437
    12
paulson@12667
    13
  InfCard       :: "i=>o"
paulson@12667
    14
    "InfCard(i) == Card(i) & nat le i"
lcp@437
    15
paulson@12667
    16
  cmult         :: "[i,i]=>i"       (infixl "|*|" 70)
paulson@12667
    17
    "i |*| j == |i*j|"
paulson@12667
    18
  
paulson@12667
    19
  cadd          :: "[i,i]=>i"       (infixl "|+|" 65)
paulson@12667
    20
    "i |+| j == |i+j|"
lcp@437
    21
paulson@12667
    22
  csquare_rel   :: "i=>i"
paulson@12667
    23
    "csquare_rel(K) ==   
paulson@12667
    24
	  rvimage(K*K,   
paulson@12667
    25
		  lam <x,y>:K*K. <x Un y, x, y>, 
paulson@12667
    26
		  rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
lcp@437
    27
lcp@484
    28
  (*This def is more complex than Kunen's but it more easily proved to
lcp@484
    29
    be a cardinal*)
paulson@12667
    30
  jump_cardinal :: "i=>i"
paulson@12667
    31
    "jump_cardinal(K) ==   
clasohm@1155
    32
         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
paulson@12667
    33
  
lcp@484
    34
  (*needed because jump_cardinal(K) might not be the successor of K*)
paulson@12667
    35
  csucc         :: "i=>i"
paulson@12667
    36
    "csucc(K) == LEAST L. Card(L) & K<L"
lcp@484
    37
wenzelm@12114
    38
syntax (xsymbols)
paulson@12667
    39
  "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
paulson@12667
    40
  "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
paulson@12667
    41
paulson@12667
    42
paulson@12667
    43
(*** The following really belong in OrderType ***)
paulson@12667
    44
paulson@12667
    45
lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
paulson@12667
    46
apply (erule trans_induct3 [of j])
paulson@12667
    47
apply (simp_all add: oadd_Limit)
paulson@12667
    48
apply (simp add: Union_empty_iff Limit_def lt_def)
paulson@12667
    49
apply blast
paulson@12667
    50
done
paulson@12667
    51
paulson@12667
    52
lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
paulson@12667
    53
by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
paulson@12667
    54
paulson@12667
    55
lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
paulson@12667
    56
apply (rule lt_trans2) 
paulson@12667
    57
apply (erule le_refl) 
paulson@12667
    58
apply (simp only: lt_Ord2  oadd_1 [of i, symmetric]) 
paulson@12667
    59
apply (blast intro: succ_leI oadd_le_mono)
paulson@12667
    60
done
paulson@12667
    61
paulson@12667
    62
lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)"
paulson@12667
    63
apply (simp add: oadd_Limit)
paulson@12667
    64
apply (frule Limit_has_1 [THEN ltD])
paulson@12667
    65
apply (rule increasing_LimitI)
paulson@12667
    66
 apply (rule Ord_0_lt)
paulson@12667
    67
  apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
paulson@12667
    68
 apply (force simp add: Union_empty_iff oadd_eq_0_iff
paulson@12667
    69
                        Limit_is_Ord [of j, THEN Ord_in_Ord])
paulson@12667
    70
apply auto
paulson@12667
    71
apply (rule_tac x="succ(x)" in bexI)
paulson@12667
    72
 apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
paulson@12667
    73
apply (simp add: Limit_def lt_def) 
paulson@12667
    74
done
paulson@12667
    75
paulson@12667
    76
(*** The following really belong in Cardinal ***)
paulson@12667
    77
paulson@12667
    78
lemma lesspoll_not_refl: "~ (i lesspoll i)"
paulson@12667
    79
by (simp add: lesspoll_def) 
paulson@12667
    80
paulson@12667
    81
lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P"
paulson@12667
    82
by (simp add: lesspoll_def) 
paulson@12667
    83
paulson@12667
    84
lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
paulson@12667
    85
apply (rule CardI) 
paulson@12667
    86
 apply (simp add: Card_is_Ord) 
paulson@12667
    87
apply (clarify dest!: ltD)
paulson@12667
    88
apply (drule bspec, assumption) 
paulson@12667
    89
apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 
paulson@12667
    90
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
paulson@12667
    91
apply (drule lesspoll_trans1, assumption) 
paulson@12667
    92
apply (subgoal_tac "B lepoll \<Union>A")
paulson@12667
    93
 apply (drule lesspoll_trans1, assumption, blast) 
paulson@12667
    94
apply (blast intro: subset_imp_lepoll) 
paulson@12667
    95
done
paulson@12667
    96
paulson@12667
    97
lemma Card_UN:
paulson@12667
    98
     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 
paulson@12667
    99
by (blast intro: Card_Union) 
paulson@12667
   100
paulson@12667
   101
lemma Card_OUN [simp,intro,TC]:
paulson@12667
   102
     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
paulson@12667
   103
by (simp add: OUnion_def Card_0) 
paulson@9654
   104
paulson@12776
   105
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
paulson@12776
   106
apply (unfold lesspoll_def)
paulson@12776
   107
apply (rule conjI)
paulson@12776
   108
apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat)
paulson@12776
   109
apply (rule notI)
paulson@12776
   110
apply (erule eqpollE)
paulson@12776
   111
apply (rule succ_lepoll_natE)
paulson@12776
   112
apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 
paulson@12776
   113
                    lepoll_trans, assumption); 
paulson@12776
   114
done
paulson@12776
   115
paulson@12776
   116
lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
paulson@12776
   117
apply (unfold lesspoll_def)
paulson@12776
   118
apply (simp add: Card_iff_initial)
paulson@12776
   119
apply (fast intro!: le_imp_lepoll ltI leI)
paulson@12776
   120
done
paulson@12776
   121
paulson@12776
   122
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
paulson@12776
   123
by (fast dest!: lepoll_0_is_0)
paulson@12776
   124
paulson@12776
   125
lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
paulson@12776
   126
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
paulson@12776
   127
paulson@12776
   128
lemma Finite_Fin_lemma [rule_format]:
paulson@12776
   129
     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
paulson@12776
   130
apply (induct_tac "n")
paulson@12776
   131
apply (rule allI)
paulson@12776
   132
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
paulson@12776
   133
apply (rule allI)
paulson@12776
   134
apply (rule impI)
paulson@12776
   135
apply (erule conjE)
paulson@12776
   136
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], (assumption))
paulson@12776
   137
apply (frule Diff_sing_eqpoll, (assumption))
paulson@12776
   138
apply (erule allE)
paulson@12776
   139
apply (erule impE, fast)
paulson@12776
   140
apply (drule subsetD, (assumption))
paulson@12776
   141
apply (drule Fin.consI, (assumption))
paulson@12776
   142
apply (simp add: cons_Diff)
paulson@12776
   143
done
paulson@12776
   144
paulson@12776
   145
lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
paulson@12776
   146
by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
paulson@12776
   147
paulson@12776
   148
lemma lesspoll_lemma: 
paulson@12776
   149
        "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
paulson@12776
   150
apply (unfold lesspoll_def)
paulson@12776
   151
apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
paulson@12776
   152
            intro!: eqpollI elim: notE 
paulson@12776
   153
            elim!: eqpollE lepoll_trans)
paulson@12776
   154
done
paulson@12776
   155
paulson@12776
   156
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
paulson@12776
   157
apply (unfold Finite_def) 
paulson@12776
   158
apply (blast intro: eqpoll_trans eqpoll_sym) 
paulson@12776
   159
done
paulson@12776
   160
lcp@437
   161
end