# HG changeset patch
# User paulson
# Date 1189776432 -7200
# Node ID 5bbdc9b6064843087e7e7b85b92656c20917a35b
# Parent  7be5353ec4bd7550a62eb32b3dd7d4b3cbcdcf84
tidied

diff -r 7be5353ec4bd -r 5bbdc9b60648 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Fri Sep 14 13:32:07 2007 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Fri Sep 14 15:27:12 2007 +0200
@@ -17,8 +17,8 @@
 
 fun fib :: "nat \<Rightarrow> nat"
 where
-     "fib 0 = 0"
-|    "fib (Suc 0) = 1"
+         "fib 0 = 0"
+|        "fib (Suc 0) = 1"
 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
 text {*
@@ -38,12 +38,13 @@
 text {* \medskip Concrete Mathematics, page 280 *}
 
 lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
-  apply (induct n rule: fib.induct)
-    prefer 3
-    txt {* simplify the LHS just enough to apply the induction hypotheses *}
-    apply (simp add: fib_Suc3)
-    apply (simp_all add: fib_2 add_mult_distrib2)
-    done
+proof (induct n rule: fib.induct)
+  case 1 show ?case by simp
+next
+  case 2 show ?case  by (simp add: fib_2)
+next
+  case 3 thus ?case by (simp add: fib_2 add_mult_distrib2)
+qed
 
 lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0"
   apply (induct n rule: fib.induct)
@@ -72,9 +73,8 @@
   case 2 thus ?case by (simp add: fib_2 mod_Suc)
 next 
   case (3 x) 
-  have th: "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
-  with prems show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2
-                   mod_Suc zmult_int [symmetric])
+  have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
+  with "3.hyps" show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2)
 qed
 
 text{*We now obtain a version for the natural numbers via the coercion 
diff -r 7be5353ec4bd -r 5bbdc9b60648 src/HOL/ex/set.thy
--- a/src/HOL/ex/set.thy	Fri Sep 14 13:32:07 2007 +0200
+++ b/src/HOL/ex/set.thy	Fri Sep 14 15:27:12 2007 +0200
@@ -43,26 +43,15 @@
 lemma singleton_example_1:
      "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   by blast
-(*With removal of negated equality literals, this no longer works:
-  by (meson subsetI subset_antisym insertCI)
-*)
 
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
   -- {*Variant of the problem above. *}
   by blast
-(*With removal of negated equality literals, this no longer works:
-by (meson subsetI subset_antisym insertCI UnionI) 
-*)
-
 
 lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
   -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
-  apply (erule ex1E, rule ex1I, erule arg_cong)
-  apply (rule subst, assumption, erule allE, rule arg_cong, erule mp)
-  apply (erule arg_cong)
-  done
-
+  by metis
 
 
 subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}