tidied
authorpaulson
Fri Sep 14 15:27:12 2007 +0200 (2007-09-14)
changeset 245735bbdc9b60648
parent 24572 7be5353ec4bd
child 24574 e840872e9c7c
tidied
src/HOL/NumberTheory/Fib.thy
src/HOL/ex/set.thy
     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Fri Sep 14 13:32:07 2007 +0200
     1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Fri Sep 14 15:27:12 2007 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4  
     1.5  fun fib :: "nat \<Rightarrow> nat"
     1.6  where
     1.7 -     "fib 0 = 0"
     1.8 -|    "fib (Suc 0) = 1"
     1.9 +         "fib 0 = 0"
    1.10 +|        "fib (Suc 0) = 1"
    1.11  | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
    1.12  
    1.13  text {*
    1.14 @@ -38,12 +38,13 @@
    1.15  text {* \medskip Concrete Mathematics, page 280 *}
    1.16  
    1.17  lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
    1.18 -  apply (induct n rule: fib.induct)
    1.19 -    prefer 3
    1.20 -    txt {* simplify the LHS just enough to apply the induction hypotheses *}
    1.21 -    apply (simp add: fib_Suc3)
    1.22 -    apply (simp_all add: fib_2 add_mult_distrib2)
    1.23 -    done
    1.24 +proof (induct n rule: fib.induct)
    1.25 +  case 1 show ?case by simp
    1.26 +next
    1.27 +  case 2 show ?case  by (simp add: fib_2)
    1.28 +next
    1.29 +  case 3 thus ?case by (simp add: fib_2 add_mult_distrib2)
    1.30 +qed
    1.31  
    1.32  lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0"
    1.33    apply (induct n rule: fib.induct)
    1.34 @@ -72,9 +73,8 @@
    1.35    case 2 thus ?case by (simp add: fib_2 mod_Suc)
    1.36  next 
    1.37    case (3 x) 
    1.38 -  have th: "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
    1.39 -  with prems show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2
    1.40 -                   mod_Suc zmult_int [symmetric])
    1.41 +  have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
    1.42 +  with "3.hyps" show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2)
    1.43  qed
    1.44  
    1.45  text{*We now obtain a version for the natural numbers via the coercion 
     2.1 --- a/src/HOL/ex/set.thy	Fri Sep 14 13:32:07 2007 +0200
     2.2 +++ b/src/HOL/ex/set.thy	Fri Sep 14 15:27:12 2007 +0200
     2.3 @@ -43,26 +43,15 @@
     2.4  lemma singleton_example_1:
     2.5       "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
     2.6    by blast
     2.7 -(*With removal of negated equality literals, this no longer works:
     2.8 -  by (meson subsetI subset_antisym insertCI)
     2.9 -*)
    2.10  
    2.11  lemma singleton_example_2:
    2.12       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    2.13    -- {*Variant of the problem above. *}
    2.14    by blast
    2.15 -(*With removal of negated equality literals, this no longer works:
    2.16 -by (meson subsetI subset_antisym insertCI UnionI) 
    2.17 -*)
    2.18 -
    2.19  
    2.20  lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
    2.21    -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
    2.22 -  apply (erule ex1E, rule ex1I, erule arg_cong)
    2.23 -  apply (rule subst, assumption, erule allE, rule arg_cong, erule mp)
    2.24 -  apply (erule arg_cong)
    2.25 -  done
    2.26 -
    2.27 +  by metis
    2.28  
    2.29  
    2.30  subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}