# HG changeset patch # User paulson # Date 1332170378 0 # Node ID 3a2e6b8a2bb8b59b15d5fd33a5207c0da09702fe # Parent f547bd4811b0c1225e9a6838c7d6e532dd26fff0 More structured proofs for cardinalities diff -r f547bd4811b0 -r 3a2e6b8a2bb8 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Mon Mar 19 10:52:48 2012 +0000 +++ b/src/ZF/Cardinal.thy Mon Mar 19 15:19:38 2012 +0000 @@ -264,9 +264,9 @@ case False hence "\x. x \ i \ ~P(x)" using step by blast - hence "(\ x. P(x)) = i" using step - by (blast intro: Least_equality elim!: ltE) - thus ?thesis using step + hence "(\ a. P(a)) = i" using step + by (blast intro: Least_equality ltD) + thus ?thesis using step.prems by simp qed qed @@ -274,16 +274,29 @@ thus ?thesis using P . qed -(*Proof is almost identical to the one above!*) -lemma Least_le: "[| P(i); Ord(i) |] ==> (\ x. P(x)) \ i" -apply (erule rev_mp) -apply (erule_tac i=i in trans_induct) -apply (rule impI) -apply (rule classical) -apply (subst Least_equality, assumption+) -apply (erule_tac [2] le_refl) -apply (blast elim: ltE intro: leI ltI lt_trans1) -done +text{*The proof is almost identical to the one above!*} +lemma Least_le: + assumes P: "P(i)" and i: "Ord(i)" shows "(\ x. P(x)) \ i" +proof - + { from i have "P(i) \ (\ x. P(x)) \ i" + proof (induct i rule: trans_induct) + case (step i) + show ?case + proof (cases "(\ a. P(a)) \ i") + case True thus ?thesis . + next + case False + hence "\x. x \ i \ ~ (\ a. P(a)) \ i" using step + by blast + hence "(\ a. P(a)) = i" using step + by (blast elim: ltE intro: ltI Least_equality lt_trans1) + thus ?thesis using step + by simp + qed + qed + } + thus ?thesis using P . +qed (*LEAST really is the smallest*) lemma less_LeastE: "[| P(i); i < (\ x. P(x)) |] ==> Q" @@ -329,12 +342,11 @@ (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) lemma well_ord_cardinal_eqpoll: - "well_ord(A,r) ==> |A| \ A" -apply (unfold cardinal_def) -apply (rule LeastI) -apply (erule_tac [2] Ord_ordertype) -apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_imp_eqpoll]) -done + assumes r: "well_ord(A,r)" shows "|A| \ A" +proof (unfold cardinal_def) + show "(\ i. i \ A) \ A" + by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) +qed (* @{term"Ord(A) ==> |A| \ A"} *) lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll] @@ -373,7 +385,7 @@ lemma CardI: "[| Ord(i); !!j. j ~(j \ i) |] ==> Card(i)" apply (unfold Card_def cardinal_def) apply (subst Least_equality) -apply (blast intro: eqpoll_refl )+ +apply (blast intro: eqpoll_refl)+ done lemma Card_is_Ord: "Card(i) ==> Ord(i)" @@ -391,14 +403,21 @@ apply (rule Ord_Least) done -(*The cardinals are the initial ordinals*) +text{*The cardinals are the initial ordinals.*} lemma Card_iff_initial: "Card(K) \ Ord(K) & (\j. j ~ j \ K)" -apply (safe intro!: CardI Card_is_Ord) - prefer 2 apply blast -apply (unfold Card_def cardinal_def) -apply (rule less_LeastE) -apply (erule_tac [2] subst, assumption+) -done +proof - + { fix j + assume K: "Card(K)" "j \ K" + assume "j < K" + also have "... = (\ i. i \ K)" using K + by (simp add: Card_def cardinal_def) + finally have "j < (\ i. i \ K)" . + hence "False" using K + by (best dest: less_LeastE) + } + then show ?thesis + by (blast intro: CardI Card_is_Ord elim:) +qed lemma lt_Card_imp_lesspoll: "[| Card(a); i i \ a" apply (unfold lesspoll_def) @@ -850,19 +869,47 @@ subsection {*Finite and infinite sets*} +lemma eqpoll_imp_Finite_iff: "A \ B ==> Finite(A) \ Finite(B)" +apply (unfold Finite_def) +apply (blast intro: eqpoll_trans eqpoll_sym) +done + lemma Finite_0 [simp]: "Finite(0)" apply (unfold Finite_def) apply (blast intro!: eqpoll_refl nat_0I) done -lemma lepoll_nat_imp_Finite: "[| A \ n; n \ nat |] ==> Finite(A)" +lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))" apply (unfold Finite_def) -apply (erule rev_mp) -apply (erule nat_induct) -apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I) -apply (blast dest!: lepoll_succ_disj) +apply (case_tac "y \ x") +apply (simp add: cons_absorb) +apply (erule bexE) +apply (rule bexI) +apply (erule_tac [2] nat_succI) +apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl) +done + +lemma Finite_succ: "Finite(x) ==> Finite(succ(x))" +apply (unfold succ_def) +apply (erule Finite_cons) done +lemma lepoll_nat_imp_Finite: + assumes A: "A \ n" and n: "n \ nat" shows "Finite(A)" +proof - + have "A \ n \ Finite(A)" using n + proof (induct n) + case 0 + hence "A = 0" by (rule lepoll_0_is_0) + thus ?case by simp + next + case (succ n) + hence "A \ n \ A \ succ(n)" by (blast dest: lepoll_succ_disj) + thus ?case using succ by (auto simp add: Finite_def) + qed + thus ?thesis using A . +qed + lemma lesspoll_nat_is_Finite: "A \ nat ==> Finite(A)" apply (unfold Finite_def) @@ -883,32 +930,17 @@ lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite] -lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \ B)" -by (blast intro: subset_Finite) - -lemmas Finite_Diff = Diff_subset [THEN subset_Finite] - -lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))" -apply (unfold Finite_def) -apply (case_tac "y \ x") -apply (simp add: cons_absorb) -apply (erule bexE) -apply (rule bexI) -apply (erule_tac [2] nat_succI) -apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl) -done - -lemma Finite_succ: "Finite(x) ==> Finite(succ(x))" -apply (unfold succ_def) -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 Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \ B)" +by (blast intro: subset_Finite) + +lemmas Finite_Diff = Diff_subset [THEN subset_Finite] + lemma nat_le_infinite_Ord: "[| Ord(i); ~ Finite(i) |] ==> nat \ i" apply (unfold Finite_def) @@ -949,11 +981,6 @@ 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 ==> \A. A \ n \ A \ Fin(A)" apply (induct_tac n) apply (simp add: eqpoll_0_iff, clarify) @@ -1074,22 +1101,30 @@ set is well-ordered. Proofs simplified by lcp. *) lemma nat_wf_on_converse_Memrel: "n \ nat ==> wf[n](converse(Memrel(n)))" -apply (erule nat_induct) -apply (blast intro: wf_onI) -apply (rule wf_onI) -apply (simp add: wf_on_def wf_def) -apply (case_tac "x \ Z") - txt{*true case*} - apply (drule_tac x = x in bspec, assumption) - apply (blast elim: mem_irrefl mem_asym) -txt{*other case*} -apply (drule_tac x = Z in spec, blast) -done +proof (induct n rule: nat_induct) + case 0 thus ?case by (blast intro: wf_onI) +next + case (succ x) + hence wfx: "\Z. Z = 0 \ (\z\Z. \y. z \ y \ z \ x \ y \ x \ z \ x \ y \ Z)" + by (simp add: wf_on_def wf_def) --{*not easy to erase the duplicate @{term"z \ x"}!*} + show ?case + proof (rule wf_onI) + fix Z u + assume Z: "u \ Z" "\z\Z. \y\Z. \y, z\ \ converse(Memrel(succ(x)))" + show False + proof (cases "x \ Z") + case True thus False using Z + by (blast elim: mem_irrefl mem_asym) + next + case False thus False using wfx [of Z] Z + by blast + qed + qed +qed lemma nat_well_ord_converse_Memrel: "n \ nat ==> well_ord(n,converse(Memrel(n)))" apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel]) -apply (unfold well_ord_def) -apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel) +apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) done lemma well_ord_converse: @@ -1122,9 +1157,7 @@ done lemma nat_into_Finite: "n \ nat ==> Finite(n)" -apply (unfold Finite_def) -apply (fast intro!: eqpoll_refl) -done + by (auto simp add: Finite_def intro: eqpoll_refl) lemma nat_not_Finite: "~ Finite(nat)" proof -