moving some results around
authorpaulson
Mon Jun 24 11:59:14 2002 +0200 (2002-06-24)
changeset 132447b37e218f298
parent 13243 ba53d07d32d5
child 13245 714f7a423a15
moving some results around
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/OrdQuant.thy
src/ZF/OrderType.thy
     1.1 --- a/src/ZF/Cardinal.thy	Mon Jun 24 11:58:21 2002 +0200
     1.2 +++ b/src/ZF/Cardinal.thy	Mon Jun 24 11:59:14 2002 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  This theory does NOT assume the Axiom of Choice
     1.5  *)
     1.6  
     1.7 -theory Cardinal = OrderType + Fixedpt + Nat + Sum:
     1.8 +theory Cardinal = OrderType + Finite + Nat + Sum:
     1.9  
    1.10  (*** The following really belong in upair ***)
    1.11  
    1.12 @@ -498,7 +498,7 @@
    1.13  
    1.14  lemma nat_lepoll_imp_le [rule_format]:
    1.15       "m:nat ==> ALL n: nat. m \<lesssim> n --> m le n"
    1.16 -apply (erule nat_induct) (*induct_tac isn't available yet*)
    1.17 +apply (induct_tac m)
    1.18  apply (blast intro!: nat_0_le)
    1.19  apply (rule ballI)
    1.20  apply (erule_tac n = "n" in natE)
    1.21 @@ -756,9 +756,9 @@
    1.22  done
    1.23  
    1.24  
    1.25 -(*** Finite and infinite sets ***)
    1.26 +subsection {*Finite and infinite sets*}
    1.27  
    1.28 -lemma Finite_0: "Finite(0)"
    1.29 +lemma Finite_0 [simp]: "Finite(0)"
    1.30  apply (unfold Finite_def)
    1.31  apply (blast intro!: eqpoll_refl nat_0I)
    1.32  done
    1.33 @@ -805,6 +805,12 @@
    1.34  apply (erule Finite_cons)
    1.35  done
    1.36  
    1.37 +lemma Finite_cons_iff [iff]:  "Finite(cons(y,x)) <-> Finite(x)"
    1.38 +by (blast intro: Finite_cons subset_Finite)
    1.39 +
    1.40 +lemma Finite_succ_iff [iff]:  "Finite(succ(x)) <-> Finite(x)"
    1.41 +by (simp add: succ_def)
    1.42 +
    1.43  lemma nat_le_infinite_Ord: 
    1.44        "[| Ord(i);  ~ Finite(i) |] ==> nat le i"
    1.45  apply (unfold Finite_def)
    1.46 @@ -819,6 +825,149 @@
    1.47  apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
    1.48  done
    1.49  
    1.50 +lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
    1.51 +by (fast dest!: lepoll_0_is_0)
    1.52 +
    1.53 +lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
    1.54 +by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
    1.55 +
    1.56 +lemma Finite_Fin_lemma [rule_format]:
    1.57 +     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
    1.58 +apply (induct_tac n)
    1.59 +apply (rule allI)
    1.60 +apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
    1.61 +apply (rule allI)
    1.62 +apply (rule impI)
    1.63 +apply (erule conjE)
    1.64 +apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
    1.65 +apply (frule Diff_sing_eqpoll, assumption)
    1.66 +apply (erule allE)
    1.67 +apply (erule impE, fast)
    1.68 +apply (drule subsetD, assumption)
    1.69 +apply (drule Fin.consI, assumption)
    1.70 +apply (simp add: cons_Diff)
    1.71 +done
    1.72 +
    1.73 +lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
    1.74 +by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
    1.75 +
    1.76 +lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
    1.77 +apply (unfold Finite_def) 
    1.78 +apply (blast intro: eqpoll_trans eqpoll_sym) 
    1.79 +done
    1.80 +
    1.81 +lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
    1.82 +apply (induct_tac n)
    1.83 +apply (simp add: eqpoll_0_iff, clarify)
    1.84 +apply (subgoal_tac "EX u. u:A")
    1.85 +apply (erule exE)
    1.86 +apply (rule Diff_sing_eqpoll [THEN revcut_rl])
    1.87 +prefer 2 apply assumption
    1.88 +apply assumption
    1.89 +apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
    1.90 +apply (rule Fin.consI, blast)
    1.91 +apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
    1.92 +(*Now for the lemma assumed above*)
    1.93 +apply (unfold eqpoll_def)
    1.94 +apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
    1.95 +done
    1.96 +
    1.97 +lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)"
    1.98 +apply (unfold Finite_def)
    1.99 +apply (blast intro: Fin_lemma)
   1.100 +done
   1.101 +
   1.102 +lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
   1.103 +by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
   1.104 +
   1.105 +lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
   1.106 +by (blast intro: Finite_into_Fin Fin_into_Finite)
   1.107 +
   1.108 +lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
   1.109 +by (blast intro!: Fin_into_Finite Fin_UnI 
   1.110 +          dest!: Finite_into_Fin
   1.111 +          intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 
   1.112 +                 Un_upper2 [THEN Fin_mono, THEN subsetD])
   1.113 +
   1.114 +lemma Finite_Union: "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))"
   1.115 +apply (simp add: Finite_Fin_iff)
   1.116 +apply (rule Fin_UnionI)
   1.117 +apply (erule Fin_induct, simp)
   1.118 +apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
   1.119 +done
   1.120 +
   1.121 +(* Induction principle for Finite(A), by Sidi Ehmety *)
   1.122 +lemma Finite_induct:
   1.123 +"[| Finite(A); P(0);
   1.124 +    !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
   1.125 + ==> P(A)"
   1.126 +apply (erule Finite_into_Fin [THEN Fin_induct]) 
   1.127 +apply (blast intro: Fin_into_Finite)+
   1.128 +done
   1.129 +
   1.130 +(*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
   1.131 +lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
   1.132 +apply (unfold Finite_def)
   1.133 +apply (case_tac "a:A")
   1.134 +apply (subgoal_tac [2] "A-{a}=A", auto)
   1.135 +apply (rule_tac x = "succ (n) " in bexI)
   1.136 +apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
   1.137 +apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
   1.138 +apply (auto dest: mem_irrefl)
   1.139 +done
   1.140 +
   1.141 +(*Sidi Ehmety.  And the contrapositive of this says
   1.142 +   [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
   1.143 +lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
   1.144 +apply (erule Finite_induct, auto)
   1.145 +apply (case_tac "x:A")
   1.146 + apply (subgoal_tac [2] "A-cons (x, B) = A - B")
   1.147 +apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
   1.148 +apply (rotate_tac -1, simp)
   1.149 +apply (drule Diff_sing_Finite, auto)
   1.150 +done
   1.151 +
   1.152 +lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
   1.153 +by (erule Finite_induct, simp_all)
   1.154 +
   1.155 +lemma Finite_RepFun_iff_lemma [rule_format]:
   1.156 +     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] 
   1.157 +      ==> \<forall>A. x = RepFun(A,f) --> Finite(A)" 
   1.158 +apply (erule Finite_induct)
   1.159 + apply clarify 
   1.160 + apply (case_tac "A=0", simp)
   1.161 + apply (blast del: allE, clarify) 
   1.162 +apply (subgoal_tac "\<exists>z\<in>A. x = f(z)") 
   1.163 + prefer 2 apply (blast del: allE elim: equalityE, clarify) 
   1.164 +apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
   1.165 + apply (blast intro: Diff_sing_Finite) 
   1.166 +apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)") 
   1.167 +apply (rule equalityI) 
   1.168 + apply (blast intro: elim: equalityE) 
   1.169 +apply (blast intro: elim: equalityCE) 
   1.170 +done
   1.171 +
   1.172 +text{*I don't know why, but if the premise is expressed using meta-connectives
   1.173 +then  the simplifier cannot prove it automatically in conditional rewriting.*}
   1.174 +lemma Finite_RepFun_iff:
   1.175 +     "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
   1.176 +by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f]) 
   1.177 +
   1.178 +lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
   1.179 +apply (erule Finite_induct) 
   1.180 +apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) 
   1.181 +done
   1.182 +
   1.183 +lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
   1.184 +apply (subgoal_tac "Finite({{x} . x \<in> A})")
   1.185 + apply (simp add: Finite_RepFun_iff ) 
   1.186 +apply (blast intro: subset_Finite) 
   1.187 +done
   1.188 +
   1.189 +lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
   1.190 +by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
   1.191 +
   1.192 +
   1.193  
   1.194  (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
   1.195    set is well-ordered.  Proofs simplified by lcp. *)
     2.1 --- a/src/ZF/CardinalArith.thy	Mon Jun 24 11:58:21 2002 +0200
     2.2 +++ b/src/ZF/CardinalArith.thy	Mon Jun 24 11:59:14 2002 +0200
     2.3 @@ -83,32 +83,6 @@
     2.4  apply (fast intro!: le_imp_lepoll ltI leI)
     2.5  done
     2.6  
     2.7 -lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
     2.8 -by (fast dest!: lepoll_0_is_0)
     2.9 -
    2.10 -lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
    2.11 -by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
    2.12 -
    2.13 -lemma Finite_Fin_lemma [rule_format]:
    2.14 -     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
    2.15 -apply (induct_tac "n")
    2.16 -apply (rule allI)
    2.17 -apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
    2.18 -apply (rule allI)
    2.19 -apply (rule impI)
    2.20 -apply (erule conjE)
    2.21 -apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
    2.22 -apply (frule Diff_sing_eqpoll, assumption)
    2.23 -apply (erule allE)
    2.24 -apply (erule impE, fast)
    2.25 -apply (drule subsetD, assumption)
    2.26 -apply (drule Fin.consI, assumption)
    2.27 -apply (simp add: cons_Diff)
    2.28 -done
    2.29 -
    2.30 -lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
    2.31 -by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
    2.32 -
    2.33  lemma lesspoll_lemma: 
    2.34          "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
    2.35  apply (unfold lesspoll_def)
    2.36 @@ -117,11 +91,6 @@
    2.37              elim!: eqpollE lepoll_trans)
    2.38  done
    2.39  
    2.40 -lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
    2.41 -apply (unfold Finite_def) 
    2.42 -apply (blast intro: eqpoll_trans eqpoll_sym) 
    2.43 -done
    2.44 -
    2.45  
    2.46  (*** Cardinal addition ***)
    2.47  
    2.48 @@ -238,7 +207,7 @@
    2.49  done
    2.50  
    2.51  lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m |+| n = m#+n"
    2.52 -apply (induct_tac "m")
    2.53 +apply (induct_tac m)
    2.54  apply (simp add: nat_into_Card [THEN cadd_0])
    2.55  apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq])
    2.56  done
    2.57 @@ -408,7 +377,7 @@
    2.58  done
    2.59  
    2.60  lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m |*| n = m#*n"
    2.61 -apply (induct_tac "m")
    2.62 +apply (induct_tac m)
    2.63  apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add)
    2.64  done
    2.65  
    2.66 @@ -801,58 +770,6 @@
    2.67                lt_csucc [THEN leI, THEN [2] le_trans])
    2.68  
    2.69  
    2.70 -(*** Finite sets ***)
    2.71 -
    2.72 -lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
    2.73 -apply (induct_tac "n")
    2.74 -apply (simp add: eqpoll_0_iff, clarify)
    2.75 -apply (subgoal_tac "EX u. u:A")
    2.76 -apply (erule exE)
    2.77 -apply (rule Diff_sing_eqpoll [THEN revcut_rl])
    2.78 -prefer 2 apply assumption
    2.79 -apply assumption
    2.80 -apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
    2.81 -apply (rule Fin.consI, blast)
    2.82 -apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
    2.83 -(*Now for the lemma assumed above*)
    2.84 -apply (unfold eqpoll_def)
    2.85 -apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
    2.86 -done
    2.87 -
    2.88 -lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)"
    2.89 -apply (unfold Finite_def)
    2.90 -apply (blast intro: Fin_lemma)
    2.91 -done
    2.92 -
    2.93 -lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
    2.94 -by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
    2.95 -
    2.96 -lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
    2.97 -by (blast intro: Finite_into_Fin Fin_into_Finite)
    2.98 -
    2.99 -lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
   2.100 -by (blast intro!: Fin_into_Finite Fin_UnI 
   2.101 -          dest!: Finite_into_Fin
   2.102 -          intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 
   2.103 -                 Un_upper2 [THEN Fin_mono, THEN subsetD])
   2.104 -
   2.105 -lemma Finite_Union: "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))"
   2.106 -apply (simp add: Finite_Fin_iff)
   2.107 -apply (rule Fin_UnionI)
   2.108 -apply (erule Fin_induct, simp)
   2.109 -apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
   2.110 -done
   2.111 -
   2.112 -(* Induction principle for Finite(A), by Sidi Ehmety *)
   2.113 -lemma Finite_induct:
   2.114 -"[| Finite(A); P(0);
   2.115 -    !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
   2.116 - ==> P(A)"
   2.117 -apply (erule Finite_into_Fin [THEN Fin_induct]) 
   2.118 -apply (blast intro: Fin_into_Finite)+
   2.119 -done
   2.120 -
   2.121 -
   2.122  (** Removing elements from a finite set decreases its cardinality **)
   2.123  
   2.124  lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A --> ~ cons(x,A) \<lesssim> A"
   2.125 @@ -906,31 +823,6 @@
   2.126  apply (simp add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl)
   2.127  done
   2.128  
   2.129 -
   2.130 -(*** Theorems by Sidi Ehmety ***)
   2.131 -
   2.132 -(*The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
   2.133 -lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
   2.134 -apply (unfold Finite_def)
   2.135 -apply (case_tac "a:A")
   2.136 -apply (subgoal_tac [2] "A-{a}=A", auto)
   2.137 -apply (rule_tac x = "succ (n) " in bexI)
   2.138 -apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
   2.139 -apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
   2.140 -apply (auto dest: mem_irrefl)
   2.141 -done
   2.142 -
   2.143 -(*And the contrapositive of this says
   2.144 -   [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
   2.145 -lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
   2.146 -apply (erule Finite_induct, auto)
   2.147 -apply (case_tac "x:A")
   2.148 - apply (subgoal_tac [2] "A-cons (x, B) = A - B")
   2.149 -apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
   2.150 -apply (rotate_tac -1, simp)
   2.151 -apply (drule Diff_sing_Finite, auto)
   2.152 -done
   2.153 -
   2.154  lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i <= nat --> i : nat | i=nat"
   2.155  apply (erule trans_induct3, auto)
   2.156  apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
     3.1 --- a/src/ZF/OrdQuant.thy	Mon Jun 24 11:58:21 2002 +0200
     3.2 +++ b/src/ZF/OrdQuant.thy	Mon Jun 24 11:59:14 2002 +0200
     3.3 @@ -58,11 +58,7 @@
     3.4  apply (blast intro: lt_Ord2) 
     3.5  done
     3.6  
     3.7 -(** Now some very basic ZF theorems **)
     3.8 -
     3.9 -(*FIXME: move to Rel.thy*)
    3.10 -lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    3.11 -by (unfold trans_def trans_on_def, blast)
    3.12 +(** Union over ordinals **)
    3.13  
    3.14  lemma Ord_OUN [intro,simp]:
    3.15       "[| !!x. x<A ==> Ord(B(x)) |] ==> Ord(\<Union>x<A. B(x))"
     4.1 --- a/src/ZF/OrderType.thy	Mon Jun 24 11:58:21 2002 +0200
     4.2 +++ b/src/ZF/OrderType.thy	Mon Jun 24 11:59:14 2002 +0200
     4.3 @@ -52,12 +52,6 @@
     4.4    "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
     4.5  
     4.6  
     4.7 -(*??for Ordinal.ML*)
     4.8 -(*suitable for rewriting PROVIDED i has been fixed*)
     4.9 -lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
    4.10 -by (blast intro: Ord_in_Ord)
    4.11 -
    4.12 -
    4.13  (**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
    4.14  
    4.15  lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"