src/ZF/CardinalArith.thy
author paulson
Wed May 08 10:12:57 2002 +0200 (2002-05-08)
changeset 13118 336b0bcbd27c
parent 12820 02e2ff3e4d37
child 13161 a40db0418145
permissions -rw-r--r--
new lemmas
     1 (*  Title:      ZF/CardinalArith.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Cardinal Arithmetic
     7 *)
     8 
     9 theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
    10 
    11 constdefs
    12 
    13   InfCard       :: "i=>o"
    14     "InfCard(i) == Card(i) & nat le i"
    15 
    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|"
    21 
    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))))"
    27 
    28   (*This def is more complex than Kunen's but it more easily proved to
    29     be a cardinal*)
    30   jump_cardinal :: "i=>i"
    31     "jump_cardinal(K) ==   
    32          UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
    33   
    34   (*needed because jump_cardinal(K) might not be the successor of K*)
    35   csucc         :: "i=>i"
    36     "csucc(K) == LEAST L. Card(L) & K<L"
    37 
    38 syntax (xsymbols)
    39   "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
    40   "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
    41 
    42 
    43 (*** The following really belong early in the development ***)
    44 
    45 lemma relation_converse_converse [simp]:
    46      "relation(r) ==> converse(converse(r)) = r"
    47 by (simp add: relation_def, blast) 
    48 
    49 lemma relation_restrict [simp]:  "relation(restrict(r,A))"
    50 by (simp add: restrict_def relation_def, blast) 
    51 
    52 (*** The following really belong in Order ***)
    53 
    54 lemma subset_ord_iso_Memrel:
    55      "\<lbrakk>f: ord_iso(A,Memrel(B),C,r); A<=B\<rbrakk> \<Longrightarrow> f: ord_iso(A,Memrel(A),C,r)"
    56 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 
    57 apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 
    58 apply (simp add: right_comp_id) 
    59 done
    60 
    61 lemma restrict_ord_iso:
    62      "\<lbrakk>f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
    63        trans[A](r)\<rbrakk>
    64       \<Longrightarrow> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
    65 apply (frule ltD) 
    66 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 
    67 apply (frule ord_iso_restrict_pred, assumption) 
    68 apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
    69 apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI]) 
    70 done
    71 
    72 lemma restrict_ord_iso2:
    73      "\<lbrakk>f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A; 
    74        j < i; trans[A](r)\<rbrakk>
    75       \<Longrightarrow> converse(restrict(converse(f), j)) 
    76           \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
    77 by (blast intro: restrict_ord_iso ord_iso_sym ltI)
    78 
    79 (*** The following really belong in OrderType ***)
    80 
    81 lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
    82 apply (erule trans_induct3 [of j])
    83 apply (simp_all add: oadd_Limit)
    84 apply (simp add: Union_empty_iff Limit_def lt_def, blast)
    85 done
    86 
    87 lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
    88 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
    89 
    90 lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
    91 apply (rule lt_trans2) 
    92 apply (erule le_refl) 
    93 apply (simp only: lt_Ord2  oadd_1 [of i, symmetric]) 
    94 apply (blast intro: succ_leI oadd_le_mono)
    95 done
    96 
    97 lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)"
    98 apply (simp add: oadd_Limit)
    99 apply (frule Limit_has_1 [THEN ltD])
   100 apply (rule increasing_LimitI)
   101  apply (rule Ord_0_lt)
   102   apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
   103  apply (force simp add: Union_empty_iff oadd_eq_0_iff
   104                         Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
   105 apply (rule_tac x="succ(x)" in bexI)
   106  apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
   107 apply (simp add: Limit_def lt_def) 
   108 done
   109 
   110 (*** The following really belong in Cardinal ***)
   111 
   112 lemma lesspoll_not_refl: "~ (i lesspoll i)"
   113 by (simp add: lesspoll_def) 
   114 
   115 lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P"
   116 by (simp add: lesspoll_def) 
   117 
   118 lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
   119 apply (rule CardI) 
   120  apply (simp add: Card_is_Ord) 
   121 apply (clarify dest!: ltD)
   122 apply (drule bspec, assumption) 
   123 apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 
   124 apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
   125 apply (drule lesspoll_trans1, assumption) 
   126 apply (subgoal_tac "B lepoll \<Union>A")
   127  apply (drule lesspoll_trans1, assumption, blast) 
   128 apply (blast intro: subset_imp_lepoll) 
   129 done
   130 
   131 lemma Card_UN:
   132      "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 
   133 by (blast intro: Card_Union) 
   134 
   135 lemma Card_OUN [simp,intro,TC]:
   136      "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
   137 by (simp add: OUnion_def Card_0) 
   138 
   139 lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
   140 apply (unfold lesspoll_def)
   141 apply (rule conjI)
   142 apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat)
   143 apply (rule notI)
   144 apply (erule eqpollE)
   145 apply (rule succ_lepoll_natE)
   146 apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 
   147                     lepoll_trans, assumption) 
   148 done
   149 
   150 lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
   151 apply (unfold lesspoll_def)
   152 apply (simp add: Card_iff_initial)
   153 apply (fast intro!: le_imp_lepoll ltI leI)
   154 done
   155 
   156 lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
   157 by (fast dest!: lepoll_0_is_0)
   158 
   159 lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
   160 by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
   161 
   162 lemma Finite_Fin_lemma [rule_format]:
   163      "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
   164 apply (induct_tac "n")
   165 apply (rule allI)
   166 apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
   167 apply (rule allI)
   168 apply (rule impI)
   169 apply (erule conjE)
   170 apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
   171 apply (frule Diff_sing_eqpoll, assumption)
   172 apply (erule allE)
   173 apply (erule impE, fast)
   174 apply (drule subsetD, assumption)
   175 apply (drule Fin.consI, assumption)
   176 apply (simp add: cons_Diff)
   177 done
   178 
   179 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
   180 by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
   181 
   182 lemma lesspoll_lemma: 
   183         "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
   184 apply (unfold lesspoll_def)
   185 apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
   186             intro!: eqpollI elim: notE 
   187             elim!: eqpollE lepoll_trans)
   188 done
   189 
   190 lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
   191 apply (unfold Finite_def) 
   192 apply (blast intro: eqpoll_trans eqpoll_sym) 
   193 done
   194 
   195 end