# HG changeset patch # User paulson # Date 1331833085 0 # Node ID d8b3412cdb999b13ce89c4a64877a996977b3078 # Parent 2b6e55924af31a67534de3a5b1e2f238a324a64c beautification and structured proofs diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/AC/HH.thy --- a/src/ZF/AC/HH.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/AC/HH.thy Thu Mar 15 17:38:05 2012 +0000 @@ -98,7 +98,7 @@ done lemma HH_subset_x_imp_lepoll: - "[| HH(f, x, i) \ Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}" + "[| HH(f, x, i) \ Pow(x)-{0}; Ord(i) |] ==> i \ Pow(x)-{0}" apply (unfold lepoll_def inj_def) apply (rule_tac x = "\j \ i. HH (f, x, j) " in exI) apply (simp (no_asm_simp)) diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/AC/WO2_AC16.thy --- a/src/ZF/AC/WO2_AC16.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/AC/WO2_AC16.thy Thu Mar 15 17:38:05 2012 +0000 @@ -177,7 +177,7 @@ done lemma Union_lesspoll: - "[| \x \ X. x lepoll n & x \ T; well_ord(T, R); X lepoll b; + "[| \x \ X. x \ n & x \ T; well_ord(T, R); X \ b; b nat |] ==> \(X)\a" apply (case_tac "Finite (X)") @@ -203,7 +203,7 @@ lemma Un_sing_eq_cons: "A \ {a} = cons(a, A)" by fast -lemma Un_lepoll_succ: "A lepoll B ==> A \ {a} lepoll succ(B)" +lemma Un_lepoll_succ: "A \ B ==> A \ {a} \ succ(B)" apply (simp add: Un_sing_eq_cons succ_def) apply (blast elim!: mem_irrefl intro: cons_lepoll_cong) done @@ -216,7 +216,7 @@ lemma recfunAC16_Diff_lepoll_1: "Ord(x) - ==> recfunAC16(f, g, x, a) - (\i recfunAC16(f, g, x, a) - (\i 1" apply (erule Ord_cases) apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll]) (*Limit case*) @@ -247,13 +247,13 @@ done -lemma two_in_lepoll_1: "[| A lepoll 1; a \ A; b \ A |] ==> a=b" +lemma two_in_lepoll_1: "[| A \ 1; a \ A; b \ A |] ==> a=b" by (fast dest!: lepoll_1_is_sing) lemma UN_lepoll_index: - "[| \ij (\xij 1; Limit(a) |] + ==> (\x a" apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]]) apply (rule_tac x = "\z \ (\x F (i) " in exI) apply (unfold inj_def) @@ -271,7 +271,7 @@ done -lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) lepoll y" +lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) \ y" apply (erule trans_induct3) (*0 case*) apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl) @@ -369,7 +369,7 @@ lemma subset_imp_eq_lemma: - "m \ nat ==> \A B. A \ B & m lepoll A & B lepoll m \ A=B" + "m \ nat ==> \A B. A \ B & m \ A & B \ m \ A=B" apply (induct_tac "m") apply (fast dest!: lepoll_0_is_0) apply (intro allI impI) @@ -385,7 +385,7 @@ done -lemma subset_imp_eq: "[| A \ B; m lepoll A; B lepoll m; m \ nat |] ==> A=B" +lemma subset_imp_eq: "[| A \ B; m \ A; B \ m; m \ nat |] ==> A=B" by (blast dest!: subset_imp_eq_lemma) diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/Cardinal_AC.thy Thu Mar 15 17:38:05 2012 +0000 @@ -11,7 +11,7 @@ subsection{*Strengthened Forms of Existing Theorems on Cardinals*} -lemma cardinal_eqpoll: "|A| eqpoll A" +lemma cardinal_eqpoll: "|A| \ A" apply (rule AC_well_ord [THEN exE]) apply (erule well_ord_cardinal_eqpoll) done @@ -19,13 +19,13 @@ text{*The theorem @{term "||A|| = |A|"} *} lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp] -lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y" +lemma cardinal_eqE: "|X| = |Y| ==> X \ Y" apply (rule AC_well_ord [THEN exE]) apply (rule AC_well_ord [THEN exE]) apply (rule well_ord_cardinal_eqE, assumption+) done -lemma cardinal_eqpoll_iff: "|X| = |Y| \ X eqpoll Y" +lemma cardinal_eqpoll_iff: "|X| = |Y| \ X \ Y" by (blast intro: cardinal_cong cardinal_eqE) lemma cardinal_disjoint_Un: @@ -33,7 +33,7 @@ ==> |A \ C| = |B \ D|" by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un) -lemma lepoll_imp_Card_le: "A lepoll B ==> |A| \ |B|" +lemma lepoll_imp_Card_le: "A \ B ==> |A| \ |B|" apply (rule AC_well_ord [THEN exE]) apply (erule well_ord_lepoll_imp_Card_le, assumption) done @@ -59,7 +59,7 @@ apply (rule well_ord_cadd_cmult_distrib, assumption+) done -lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A" +lemma InfCard_square_eq: "InfCard(|A|) ==> A*A \ A" apply (rule AC_well_ord [THEN exE]) apply (erule well_ord_InfCard_square_eq, assumption) done @@ -67,36 +67,50 @@ subsection {*The relationship between cardinality and le-pollence*} -lemma Card_le_imp_lepoll: "|A| \ |B| ==> A lepoll B" -apply (rule cardinal_eqpoll - [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans]) -apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans]) -apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll]) -done +lemma Card_le_imp_lepoll: + assumes "|A| \ |B|" shows "A \ B" +proof - + have "A \ |A|" + by (rule cardinal_eqpoll [THEN eqpoll_sym]) + also have "... \ |B|" + by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms) + also have "... \ B" + by (rule cardinal_eqpoll) + finally show ?thesis . +qed -lemma le_Card_iff: "Card(K) ==> |A| \ K \ A lepoll K" +lemma le_Card_iff: "Card(K) ==> |A| \ K \ A \ K" apply (erule Card_cardinal_eq [THEN subst], rule iffI, erule Card_le_imp_lepoll) apply (erule lepoll_imp_Card_le) done -lemma cardinal_0_iff_0 [simp]: "|A| = 0 \ A = 0"; +lemma cardinal_0_iff_0 [simp]: "|A| = 0 \ A = 0" apply auto apply (drule cardinal_0 [THEN ssubst]) apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1]) done -lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| \ i lesspoll A" -apply (cut_tac A = "A" in cardinal_eqpoll) -apply (auto simp add: eqpoll_iff) -apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal) -apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2 - simp add: cardinal_idem) -done +lemma cardinal_lt_iff_lesspoll: + assumes i: "Ord(i)" shows "i < |A| \ i \ A" +proof + assume "i < |A|" + hence "i \ |A|" + by (blast intro: lt_Card_imp_lesspoll Card_cardinal) + also have "... \ A" + by (rule cardinal_eqpoll) + finally show "i \ A" . +next + assume "i \ A" + also have "... \ |A|" + by (blast intro: cardinal_eqpoll eqpoll_sym) + finally have "i \ |A|" . + thus "i < |A|" using i + by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt) +qed lemma cardinal_le_imp_lepoll: " i \ |A| ==> i \ A" -apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans) -done + by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans) subsection{*Other Applications of AC*} @@ -164,15 +178,21 @@ set need not be a cardinal. Surprisingly complicated proof! **) -(*Work backwards along the injection from W into K, given that @{term"W\0"}.*) +text{*Work backwards along the injection from @{term W} into @{term K}, given that @{term"W\0"}.*} + lemma inj_UN_subset: - "[| f: inj(A,B); a:A |] ==> - (\x\A. C(x)) \ (\y\B. C(if y: range(f) then converse(f)`y else a))" -apply (rule UN_least) -apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper]) - apply (simp add: inj_is_fun [THEN apply_rangeI]) -apply (blast intro: inj_is_fun [THEN apply_type]) -done + assumes f: "f \ inj(A,B)" and a: "a \ A" + shows "(\x\A. C(x)) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))" +proof (rule UN_least) + fix x + assume x: "x \ A" + hence fx: "f ` x \ B" by (blast intro: f inj_is_fun [THEN apply_type]) + have "C(x) \ C(if f ` x \ range(f) then converse(f) ` (f ` x) else a)" + using f x by (simp add: inj_is_fun [THEN apply_rangeI]) + also have "... \ (\y\B. C(if y \ range(f) then converse(f) ` y else a))" + by (rule UN_upper [OF fx]) + finally show "C(x) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))" . +qed (*Simpler to require |W|=K; we'd have a bijection; but the theorem would be weaker.*) diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/Nat_ZF.thy --- a/src/ZF/Nat_ZF.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/Nat_ZF.thy Thu Mar 15 17:38:05 2012 +0000 @@ -92,7 +92,7 @@ lemma natE: assumes "n \ nat" - obtains (0) "n=0" | (succ) x where "x \ nat" "n=succ(x)" + obtains ("0") "n=0" | (succ) x where "x \ nat" "n=succ(x)" using assms by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/Ordinal.thy --- a/src/ZF/Ordinal.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/Ordinal.thy Thu Mar 15 17:38:05 2012 +0000 @@ -703,7 +703,7 @@ lemma Ord_cases: assumes i: "Ord(i)" - obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)" + obtains ("0") "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)" by (insert Ord_cases_disj [OF i], auto) lemma trans_induct3_raw: diff -r 2b6e55924af3 -r d8b3412cdb99 src/ZF/UNITY/AllocBase.thy --- a/src/ZF/UNITY/AllocBase.thy Thu Mar 15 16:35:02 2012 +0000 +++ b/src/ZF/UNITY/AllocBase.thy Thu Mar 15 17:38:05 2012 +0000 @@ -342,7 +342,7 @@ apply (simp add: length_nat_list_inj) done -lemma nat_lepoll_var: "nat lepoll var" +lemma nat_lepoll_var: "nat \ var" apply (unfold lepoll_def) apply (rule_tac x = " (\x\nat. nat_var_inj (x))" in exI) apply (rule var_infinite_lemma)