# HG changeset patch # User paulson # Date 1024912754 -7200 # Node ID 7b37e218f298ac6f650d158b58b4095f11ff58a3 # Parent ba53d07d32d53359c3661aaeadc7bb1c71525d8d moving some results around diff -r ba53d07d32d5 -r 7b37e218f298 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Mon Jun 24 11:58:21 2002 +0200 +++ b/src/ZF/Cardinal.thy Mon Jun 24 11:59:14 2002 +0200 @@ -8,7 +8,7 @@ This theory does NOT assume the Axiom of Choice *) -theory Cardinal = OrderType + Fixedpt + Nat + Sum: +theory Cardinal = OrderType + Finite + Nat + Sum: (*** The following really belong in upair ***) @@ -498,7 +498,7 @@ lemma nat_lepoll_imp_le [rule_format]: "m:nat ==> ALL n: nat. m \ n --> m le n" -apply (erule nat_induct) (*induct_tac isn't available yet*) +apply (induct_tac m) apply (blast intro!: nat_0_le) apply (rule ballI) apply (erule_tac n = "n" in natE) @@ -756,9 +756,9 @@ done -(*** Finite and infinite sets ***) +subsection {*Finite and infinite sets*} -lemma Finite_0: "Finite(0)" +lemma Finite_0 [simp]: "Finite(0)" apply (unfold Finite_def) apply (blast intro!: eqpoll_refl nat_0I) done @@ -805,6 +805,12 @@ apply (erule Finite_cons) done +lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)" +by (blast intro: Finite_cons subset_Finite) + +lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)" +by (simp add: succ_def) + lemma nat_le_infinite_Ord: "[| Ord(i); ~ Finite(i) |] ==> nat le i" apply (unfold Finite_def) @@ -819,6 +825,149 @@ apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord) done +lemma succ_lepoll_imp_not_empty: "succ(x) \ y ==> y \ 0" +by (fast dest!: lepoll_0_is_0) + +lemma eqpoll_succ_imp_not_empty: "x \ succ(n) ==> x \ 0" +by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0]) + +lemma Finite_Fin_lemma [rule_format]: + "n \ nat ==> \A. (A\n & A \ X) --> A \ Fin(X)" +apply (induct_tac n) +apply (rule allI) +apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) +apply (rule allI) +apply (rule impI) +apply (erule conjE) +apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption) +apply (frule Diff_sing_eqpoll, assumption) +apply (erule allE) +apply (erule impE, fast) +apply (drule subsetD, assumption) +apply (drule Fin.consI, assumption) +apply (simp add: cons_Diff) +done + +lemma Finite_Fin: "[| Finite(A); A \ X |] ==> A \ Fin(X)" +by (unfold Finite_def, blast intro: Finite_Fin_lemma) + +lemma eqpoll_imp_Finite_iff: "A \ B ==> Finite(A) <-> Finite(B)" +apply (unfold Finite_def) +apply (blast intro: eqpoll_trans eqpoll_sym) +done + +lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \ n --> A : Fin(A)" +apply (induct_tac n) +apply (simp add: eqpoll_0_iff, clarify) +apply (subgoal_tac "EX u. u:A") +apply (erule exE) +apply (rule Diff_sing_eqpoll [THEN revcut_rl]) +prefer 2 apply assumption +apply assumption +apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption) +apply (rule Fin.consI, blast) +apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) +(*Now for the lemma assumed above*) +apply (unfold eqpoll_def) +apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type]) +done + +lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)" +apply (unfold Finite_def) +apply (blast intro: Fin_lemma) +done + +lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)" +by (fast intro!: Finite_0 Finite_cons elim: Fin_induct) + +lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)" +by (blast intro: Finite_into_Fin Fin_into_Finite) + +lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)" +by (blast intro!: Fin_into_Finite Fin_UnI + dest!: Finite_into_Fin + intro: Un_upper1 [THEN Fin_mono, THEN subsetD] + Un_upper2 [THEN Fin_mono, THEN subsetD]) + +lemma Finite_Union: "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))" +apply (simp add: Finite_Fin_iff) +apply (rule Fin_UnionI) +apply (erule Fin_induct, simp) +apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD]) +done + +(* Induction principle for Finite(A), by Sidi Ehmety *) +lemma Finite_induct: +"[| Finite(A); P(0); + !! x B. [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |] + ==> P(A)" +apply (erule Finite_into_Fin [THEN Fin_induct]) +apply (blast intro: Fin_into_Finite)+ +done + +(*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) +lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" +apply (unfold Finite_def) +apply (case_tac "a:A") +apply (subgoal_tac [2] "A-{a}=A", auto) +apply (rule_tac x = "succ (n) " in bexI) +apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ") +apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong) +apply (auto dest: mem_irrefl) +done + +(*Sidi Ehmety. And the contrapositive of this says + [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *) +lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)" +apply (erule Finite_induct, auto) +apply (case_tac "x:A") + apply (subgoal_tac [2] "A-cons (x, B) = A - B") +apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}") +apply (rotate_tac -1, simp) +apply (drule Diff_sing_Finite, auto) +done + +lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))" +by (erule Finite_induct, simp_all) + +lemma Finite_RepFun_iff_lemma [rule_format]: + "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] + ==> \A. x = RepFun(A,f) --> Finite(A)" +apply (erule Finite_induct) + apply clarify + apply (case_tac "A=0", simp) + apply (blast del: allE, clarify) +apply (subgoal_tac "\z\A. x = f(z)") + prefer 2 apply (blast del: allE elim: equalityE, clarify) +apply (subgoal_tac "B = {f(u) . u \ A - {z}}") + apply (blast intro: Diff_sing_Finite) +apply (thin_tac "\A. ?P(A) --> Finite(A)") +apply (rule equalityI) + apply (blast intro: elim: equalityE) +apply (blast intro: elim: equalityCE) +done + +text{*I don't know why, but if the premise is expressed using meta-connectives +then the simplifier cannot prove it automatically in conditional rewriting.*} +lemma Finite_RepFun_iff: + "(\x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)" +by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f]) + +lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))" +apply (erule Finite_induct) +apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) +done + +lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)" +apply (subgoal_tac "Finite({{x} . x \ A})") + apply (simp add: Finite_RepFun_iff ) +apply (blast intro: subset_Finite) +done + +lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)" +by (blast intro: Finite_Pow Finite_Pow_imp_Finite) + + (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered set is well-ordered. Proofs simplified by lcp. *) diff -r ba53d07d32d5 -r 7b37e218f298 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Mon Jun 24 11:58:21 2002 +0200 +++ b/src/ZF/CardinalArith.thy Mon Jun 24 11:59:14 2002 +0200 @@ -83,32 +83,6 @@ apply (fast intro!: le_imp_lepoll ltI leI) done -lemma succ_lepoll_imp_not_empty: "succ(x) \ y ==> y \ 0" -by (fast dest!: lepoll_0_is_0) - -lemma eqpoll_succ_imp_not_empty: "x \ succ(n) ==> x \ 0" -by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0]) - -lemma Finite_Fin_lemma [rule_format]: - "n \ nat ==> \A. (A\n & A \ X) --> A \ Fin(X)" -apply (induct_tac "n") -apply (rule allI) -apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) -apply (rule allI) -apply (rule impI) -apply (erule conjE) -apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption) -apply (frule Diff_sing_eqpoll, assumption) -apply (erule allE) -apply (erule impE, fast) -apply (drule subsetD, assumption) -apply (drule Fin.consI, assumption) -apply (simp add: cons_Diff) -done - -lemma Finite_Fin: "[| Finite(A); A \ X |] ==> A \ Fin(X)" -by (unfold Finite_def, blast intro: Finite_Fin_lemma) - lemma lesspoll_lemma: "[| ~ A \ B; C \ B |] ==> A - C \ 0" apply (unfold lesspoll_def) @@ -117,11 +91,6 @@ elim!: eqpollE lepoll_trans) done -lemma eqpoll_imp_Finite_iff: "A \ B ==> Finite(A) <-> Finite(B)" -apply (unfold Finite_def) -apply (blast intro: eqpoll_trans eqpoll_sym) -done - (*** Cardinal addition ***) @@ -238,7 +207,7 @@ done lemma nat_cadd_eq_add: "[| m: nat; n: nat |] ==> m |+| n = m#+n" -apply (induct_tac "m") +apply (induct_tac m) apply (simp add: nat_into_Card [THEN cadd_0]) apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq]) done @@ -408,7 +377,7 @@ done lemma nat_cmult_eq_mult: "[| m: nat; n: nat |] ==> m |*| n = m#*n" -apply (induct_tac "m") +apply (induct_tac m) apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add) done @@ -801,58 +770,6 @@ lt_csucc [THEN leI, THEN [2] le_trans]) -(*** Finite sets ***) - -lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \ n --> A : Fin(A)" -apply (induct_tac "n") -apply (simp add: eqpoll_0_iff, clarify) -apply (subgoal_tac "EX u. u:A") -apply (erule exE) -apply (rule Diff_sing_eqpoll [THEN revcut_rl]) -prefer 2 apply assumption -apply assumption -apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption) -apply (rule Fin.consI, blast) -apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD]) -(*Now for the lemma assumed above*) -apply (unfold eqpoll_def) -apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type]) -done - -lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)" -apply (unfold Finite_def) -apply (blast intro: Fin_lemma) -done - -lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)" -by (fast intro!: Finite_0 Finite_cons elim: Fin_induct) - -lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)" -by (blast intro: Finite_into_Fin Fin_into_Finite) - -lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)" -by (blast intro!: Fin_into_Finite Fin_UnI - dest!: Finite_into_Fin - intro: Un_upper1 [THEN Fin_mono, THEN subsetD] - Un_upper2 [THEN Fin_mono, THEN subsetD]) - -lemma Finite_Union: "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))" -apply (simp add: Finite_Fin_iff) -apply (rule Fin_UnionI) -apply (erule Fin_induct, simp) -apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD]) -done - -(* Induction principle for Finite(A), by Sidi Ehmety *) -lemma Finite_induct: -"[| Finite(A); P(0); - !! x B. [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |] - ==> P(A)" -apply (erule Finite_into_Fin [THEN Fin_induct]) -apply (blast intro: Fin_into_Finite)+ -done - - (** Removing elements from a finite set decreases its cardinality **) lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A --> ~ cons(x,A) \ A" @@ -906,31 +823,6 @@ apply (simp add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl) done - -(*** Theorems by Sidi Ehmety ***) - -(*The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *) -lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)" -apply (unfold Finite_def) -apply (case_tac "a:A") -apply (subgoal_tac [2] "A-{a}=A", auto) -apply (rule_tac x = "succ (n) " in bexI) -apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ") -apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong) -apply (auto dest: mem_irrefl) -done - -(*And the contrapositive of this says - [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *) -lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)" -apply (erule Finite_induct, auto) -apply (case_tac "x:A") - apply (subgoal_tac [2] "A-cons (x, B) = A - B") -apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}") -apply (rotate_tac -1, simp) -apply (drule Diff_sing_Finite, auto) -done - lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i <= nat --> i : nat | i=nat" apply (erule trans_induct3, auto) apply (blast dest!: nat_le_Limit [THEN le_imp_subset]) diff -r ba53d07d32d5 -r 7b37e218f298 src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Mon Jun 24 11:58:21 2002 +0200 +++ b/src/ZF/OrdQuant.thy Mon Jun 24 11:59:14 2002 +0200 @@ -58,11 +58,7 @@ apply (blast intro: lt_Ord2) done -(** Now some very basic ZF theorems **) - -(*FIXME: move to Rel.thy*) -lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)" -by (unfold trans_def trans_on_def, blast) +(** Union over ordinals **) lemma Ord_OUN [intro,simp]: "[| !!x. x Ord(B(x)) |] ==> Ord(\x i" (infixl "\\" 70) -(*??for Ordinal.ML*) -(*suitable for rewriting PROVIDED i has been fixed*) -lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)" -by (blast intro: Ord_in_Ord) - - (**** Proofs needing the combination of Ordinal.thy and Order.thy ****) lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"