Rewrote some induction proofs to be structured
authorpaulson
Thu Mar 15 15:54:22 2012 +0000 (2012-03-15)
changeset 469525e1bcfdcb175
parent 46937 efb98d27dc1a
child 46953 2b6e55924af3
Rewrote some induction proofs to be structured
src/ZF/CardinalArith.thy
     1.1 --- a/src/ZF/CardinalArith.thy	Wed Mar 14 22:34:18 2012 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Thu Mar 15 15:54:22 2012 +0000
     1.3 @@ -154,13 +154,16 @@
     1.4  (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
     1.5  
     1.6  lemma cadd_le_self:
     1.7 -    "[| Card(K);  Ord(L) |] ==> K \<le> (K \<oplus> L)"
     1.8 -apply (unfold cadd_def)
     1.9 -apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le],
    1.10 -       assumption)
    1.11 -apply (rule_tac [2] sum_lepoll_self)
    1.12 -apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord)
    1.13 -done
    1.14 +  assumes K: "Card(K)" and L: "Ord(L)" shows "K \<le> (K \<oplus> L)"
    1.15 +proof (unfold cadd_def)
    1.16 +  have "K \<le> |K|"
    1.17 +    by (rule Card_cardinal_le [OF K]) 
    1.18 +  moreover have "|K| \<le> |K + L|" using K L
    1.19 +    by (blast intro: well_ord_lepoll_imp_Card_le sum_lepoll_self
    1.20 +                     well_ord_radd well_ord_Memrel Card_is_Ord) 
    1.21 +  ultimately show "K \<le> |K + L|" 
    1.22 +    by (blast intro: le_trans) 
    1.23 +qed
    1.24  
    1.25  subsubsection{*Monotonicity of addition*}
    1.26  
    1.27 @@ -197,19 +200,26 @@
    1.28  (*Pulling the  succ(...)  outside the |...| requires m, n: nat  *)
    1.29  (*Unconditional version requires AC*)
    1.30  lemma cadd_succ_lemma:
    1.31 -    "[| Ord(m);  Ord(n) |] ==> succ(m) \<oplus> n = |succ(m \<oplus> n)|"
    1.32 -apply (unfold cadd_def)
    1.33 -apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans])
    1.34 -apply (rule succ_eqpoll_cong [THEN cardinal_cong])
    1.35 -apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym])
    1.36 -apply (blast intro: well_ord_radd well_ord_Memrel)
    1.37 -done
    1.38 +  assumes "Ord(m)" "Ord(n)" shows "succ(m) \<oplus> n = |succ(m \<oplus> n)|"
    1.39 +proof (unfold cadd_def)
    1.40 +  have [intro]: "m + n \<approx> |m + n|" using assms
    1.41 +    by (blast intro: eqpoll_sym well_ord_cardinal_eqpoll well_ord_radd well_ord_Memrel)
    1.42  
    1.43 -lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m \<oplus> n = m#+n"
    1.44 -apply (induct_tac m)
    1.45 -apply (simp add: nat_into_Card [THEN cadd_0])
    1.46 -apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq])
    1.47 -done
    1.48 +  have "|succ(m) + n| = |succ(m + n)|"
    1.49 +    by (rule sum_succ_eqpoll [THEN cardinal_cong]) 
    1.50 +  also have "... = |succ(|m + n|)|" 
    1.51 +    by (blast intro: succ_eqpoll_cong cardinal_cong)
    1.52 +  finally show "|succ(m) + n| = |succ(|m + n|)|" .
    1.53 +qed
    1.54 +
    1.55 +lemma nat_cadd_eq_add:
    1.56 +  assumes m: "m: nat" and [simp]: "n: nat" shows"m \<oplus> n = m #+ n"
    1.57 +using m
    1.58 +proof (induct m)
    1.59 +  case 0 thus ?case by (simp add: nat_into_Card cadd_0)
    1.60 +next
    1.61 +  case (succ m) thus ?case by (simp add: cadd_succ_lemma nat_into_Card Card_cardinal_eq)
    1.62 +qed
    1.63  
    1.64  
    1.65  subsection{*Cardinal multiplication*}
    1.66 @@ -826,32 +836,40 @@
    1.67  
    1.68  subsubsection{*Removing elements from a finite set decreases its cardinality*}
    1.69  
    1.70 -lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x\<notin>A \<longrightarrow> ~ cons(x,A) \<lesssim> A"
    1.71 -apply (erule Fin_induct)
    1.72 -apply (simp add: lepoll_0_iff)
    1.73 -apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))")
    1.74 -apply simp
    1.75 -apply (blast dest!: cons_lepoll_consD, blast)
    1.76 -done
    1.77 -
    1.78  lemma Finite_imp_cardinal_cons [simp]:
    1.79 -     "[| Finite(A);  a\<notin>A |] ==> |cons(a,A)| = succ(|A|)"
    1.80 -apply (unfold cardinal_def)
    1.81 -apply (rule Least_equality)
    1.82 -apply (fold cardinal_def)
    1.83 -apply (simp add: succ_def)
    1.84 -apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll
    1.85 -             elim!: mem_irrefl  dest!: Finite_imp_well_ord)
    1.86 -apply (blast intro: Card_cardinal Card_is_Ord)
    1.87 -apply (rule notI)
    1.88 -apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE],
    1.89 -       assumption, assumption)
    1.90 -apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
    1.91 -apply (erule le_imp_lepoll [THEN lepoll_trans])
    1.92 -apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll]
    1.93 -             dest!: Finite_imp_well_ord)
    1.94 -done
    1.95 -
    1.96 +  assumes FA: "Finite(A)" and a: "a\<notin>A" shows "|cons(a,A)| = succ(|A|)"
    1.97 +proof -
    1.98 +  { fix X
    1.99 +    have "Finite(X) ==> a \<notin> X \<Longrightarrow> cons(a,X) \<lesssim> X \<Longrightarrow> False"
   1.100 +      proof (induct X rule: Finite_induct)
   1.101 +        case 0 thus False  by (simp add: lepoll_0_iff) 
   1.102 +      next
   1.103 +        case (cons x Y) 
   1.104 +        hence "cons(x, cons(a, Y)) \<lesssim> cons(x, Y)" by (simp add: cons_commute) 
   1.105 +        hence "cons(a, Y) \<lesssim> Y" using cons        by (blast dest: cons_lepoll_consD)
   1.106 +        thus False using cons by auto
   1.107 +      qed
   1.108 +  } 
   1.109 +  hence [simp]: "~ cons(a,A) \<lesssim> A" using a FA by auto
   1.110 +  have [simp]: "|A| \<approx> A" using Finite_imp_well_ord [OF FA]
   1.111 +    by (blast intro: well_ord_cardinal_eqpoll)
   1.112 +  have "(\<mu> i. i \<approx> cons(a, A)) = succ(|A|)" 
   1.113 +    proof (rule Least_equality [OF _ _ notI])
   1.114 +      show "succ(|A|) \<approx> cons(a, A)" 
   1.115 +        by (simp add: succ_def cons_eqpoll_cong mem_not_refl a) 
   1.116 +    next
   1.117 +      show "Ord(succ(|A|))" by simp
   1.118 +    next
   1.119 +      fix i
   1.120 +      assume i: "i \<le> |A|" "i \<approx> cons(a, A)"
   1.121 +      have "cons(a, A) \<approx> i" by (rule eqpoll_sym) (rule i)
   1.122 +      also have "... \<lesssim> |A|" by (rule le_imp_lepoll) (rule i)
   1.123 +      also have "... \<approx> A"   by simp
   1.124 +      finally have "cons(a, A) \<lesssim> A" .
   1.125 +      thus False by simp
   1.126 +    qed
   1.127 +  thus ?thesis by (simp add: cardinal_def) 
   1.128 +qed
   1.129  
   1.130  lemma Finite_imp_succ_cardinal_Diff:
   1.131       "[| Finite(A);  a:A |] ==> succ(|A-{a}|) = |A|"
   1.132 @@ -866,9 +884,11 @@
   1.133  done
   1.134  
   1.135  lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| \<in> nat"
   1.136 -apply (erule Finite_induct)
   1.137 -apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons)
   1.138 -done
   1.139 +proof (induct rule: Finite_induct)
   1.140 +  case 0 thus ?case by (simp add: cardinal_0)
   1.141 +next
   1.142 +  case (cons x A) thus ?case by (simp add: Finite_imp_cardinal_cons)
   1.143 +qed
   1.144  
   1.145  lemma card_Un_Int:
   1.146       "[|Finite(A); Finite(B)|] ==> |A| #+ |B| = |A \<union> B| #+ |A \<inter> B|"
   1.147 @@ -880,17 +900,22 @@
   1.148       "[|Finite(A); Finite(B); A \<inter> B = 0|] ==> |A \<union> B| = |A| #+ |B|"
   1.149  by (simp add: Finite_Un card_Un_Int)
   1.150  
   1.151 -lemma card_partition [rule_format]:
   1.152 -     "Finite(C) ==>
   1.153 -        Finite (\<Union> C) \<longrightarrow>
   1.154 -        (\<forall>c\<in>C. |c| = k) \<longrightarrow>
   1.155 -        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = 0) \<longrightarrow>
   1.156 +lemma card_partition:
   1.157 +  assumes FC: "Finite(C)"
   1.158 +  shows
   1.159 +     "Finite (\<Union> C) \<Longrightarrow>
   1.160 +        (\<forall>c\<in>C. |c| = k) \<Longrightarrow>
   1.161 +        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = 0) \<Longrightarrow>
   1.162          k #* |C| = |\<Union> C|"
   1.163 -apply (erule Finite_induct, auto)
   1.164 -apply (subgoal_tac " x \<inter> \<Union>B = 0")
   1.165 -apply (auto simp add: card_Un_disjoint Finite_Union
   1.166 -       subset_Finite [of _ "\<Union> (cons(x,F))"])
   1.167 -done
   1.168 +using FC
   1.169 +proof (induct rule: Finite_induct)
   1.170 +  case 0 thus ?case by simp
   1.171 +next
   1.172 +  case (cons x B)
   1.173 +  hence "x \<inter> \<Union>B = 0" by auto
   1.174 +  thus ?case using cons
   1.175 +    by (auto simp add: card_Un_disjoint)
   1.176 +qed
   1.177  
   1.178  
   1.179  subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*}
   1.180 @@ -920,39 +945,4 @@
   1.181  lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)"
   1.182  by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
   1.183  
   1.184 -lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1"
   1.185 -apply (rule succ_inject)
   1.186 -apply (rule_tac b = "|A|" in trans)
   1.187 - apply (simp add: Finite_imp_succ_cardinal_Diff)
   1.188 -apply (subgoal_tac "1 \<lesssim> A")
   1.189 - prefer 2 apply (blast intro: not_0_is_lepoll_1)
   1.190 -apply (frule Finite_imp_well_ord, clarify)
   1.191 -apply (drule well_ord_lepoll_imp_Card_le)
   1.192 - apply (auto simp add: cardinal_1)
   1.193 -apply (rule trans)
   1.194 - apply (rule_tac [2] diff_succ)
   1.195 -  apply (auto simp add: Finite_cardinal_in_nat)
   1.196 -done
   1.197 -
   1.198 -lemma cardinal_lt_imp_Diff_not_0 [rule_format]:
   1.199 -     "Finite(B) ==> \<forall>A. |B|<|A| \<longrightarrow> A - B \<noteq> 0"
   1.200 -apply (erule Finite_induct, auto)
   1.201 -apply (case_tac "Finite (A)")
   1.202 - apply (subgoal_tac [2] "Finite (cons (x, B))")
   1.203 -  apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite)
   1.204 -   apply (auto simp add: Finite_0 Finite_cons)
   1.205 -apply (subgoal_tac "|B|<|A|")
   1.206 - prefer 2 apply (blast intro: lt_trans Ord_cardinal)
   1.207 -apply (case_tac "x:A")
   1.208 - apply (subgoal_tac [2] "A - cons (x, B) = A - B")
   1.209 -  apply auto
   1.210 -apply (subgoal_tac "|A| \<le> |cons (x, B) |")
   1.211 - prefer 2
   1.212 - apply (blast dest: Finite_cons [THEN Finite_imp_well_ord]
   1.213 -              intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll)
   1.214 -apply (auto simp add: Finite_imp_cardinal_cons)
   1.215 -apply (auto dest!: Finite_cardinal_in_nat simp add: le_iff)
   1.216 -apply (blast intro: lt_trans)
   1.217 -done
   1.218 -
   1.219  end