author paulson Fri, 14 Sep 2007 15:27:12 +0200 changeset 24573 5bbdc9b60648 parent 24572 7be5353ec4bd child 24574 e840872e9c7c
tidied
 src/HOL/NumberTheory/Fib.thy file | annotate | diff | comparison | revisions src/HOL/ex/set.thy file | annotate | diff | comparison | revisions
```--- 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 *}
-    done
+proof (induct n rule: fib.induct)
+  case 1 show ?case by simp
+next
+  case 2 show ?case  by (simp add: fib_2)
+next
+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
-                   mod_Suc zmult_int [symmetric])
+  have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
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 *}```