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