--- 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
--- 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 *}