tuned proof;
authorwenzelm
Sun Jan 29 13:43:17 2017 +0100 (2017-01-29)
changeset 64964a0c985a57f7e
parent 64963 fc4d1ceb8e29
child 64965 d55d743c45a2
tuned proof;
src/HOL/Power.thy
     1.1 --- a/src/HOL/Power.thy	Sun Jan 29 13:28:45 2017 +0100
     1.2 +++ b/src/HOL/Power.thy	Sun Jan 29 13:43:17 2017 +0100
     1.3 @@ -596,7 +596,7 @@
     1.4  
     1.5  lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
     1.6    by (induct n) (simp_all add: sgn_mult)
     1.7 -    
     1.8 +
     1.9  lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
    1.10    by (simp add: power_abs)
    1.11  
    1.12 @@ -842,18 +842,24 @@
    1.13  lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
    1.14  proof (induct rule: finite_induct)
    1.15    case empty
    1.16 -  show ?case by auto
    1.17 +  show ?case by simp
    1.18  next
    1.19    case (insert x A)
    1.20 -  then have "inj_on (insert x) (Pow A)"
    1.21 -    unfolding inj_on_def by (blast elim!: equalityE)
    1.22 -  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
    1.23 -    by (simp add: mult_2 card_image Pow_insert insert.hyps)
    1.24 -  with insert show ?case
    1.25 -    apply (simp add: Pow_insert)
    1.26 -    apply (subst card_Un_disjoint)
    1.27 -       apply auto
    1.28 -    done
    1.29 +  from \<open>x \<notin> A\<close> have disjoint: "Pow A \<inter> insert x ` Pow A = {}" by blast
    1.30 +  from \<open>x \<notin> A\<close> have inj_on: "inj_on (insert x) (Pow A)"
    1.31 +    unfolding inj_on_def by auto
    1.32 +
    1.33 +  have "card (Pow (insert x A)) = card (Pow A \<union> insert x ` Pow A)"
    1.34 +    by (simp only: Pow_insert)
    1.35 +  also have "\<dots> = card (Pow A) + card (insert x ` Pow A)"
    1.36 +    by (rule card_Un_disjoint) (use \<open>finite A\<close> disjoint in simp_all)
    1.37 +  also from inj_on have "card (insert x ` Pow A) = card (Pow A)"
    1.38 +    by (rule card_image)
    1.39 +  also have "\<dots> + \<dots> = 2 * \<dots>" by (simp add: mult_2)
    1.40 +  also from insert(3) have "\<dots> = 2 ^ Suc (card A)" by simp
    1.41 +  also from insert(1,2) have "Suc (card A) = card (insert x A)"
    1.42 +    by (rule card_insert_disjoint [symmetric])
    1.43 +  finally show ?case .
    1.44  qed
    1.45  
    1.46