Update some examples

1 files changed, 81 insertions, 64 deletions

diff --git a/etc/isar/Fibonacci.thy b/etc/isar/Fibonacci.thy
index 0cbc8090..8e57b459 100644
--- a/etc/isar/Fibonacci.thy
+++ b/etc/isar/Fibonacci.thy
@@ -1,25 +1,47 @@
-(* Fibonacci.thy taken from Isabelle distribution
-   Gertrud Bauer / Larry Paulson  *)
+(*  Title:      HOL/Isar_examples/Fibonacci.thy
+    ID:         $Id$
+    Author:     Gertrud Bauer
+    Copyright   1999 Technische Universitaet Muenchen
+
+The Fibonacci function.  Demonstrates the use of recdef.  Original
+tactic script by Lawrence C Paulson.
+
+Fibonacci numbers: proofs of laws taken from
+
+  R. L. Graham, D. E. Knuth, O. Patashnik.
+  Concrete Mathematics.
+  (Addison-Wesley, 1989)
+*)
+
+header {* Fib and Gcd commute *}
+
+theory Fibonacci
+imports Primes
+begin
+
+text_raw {*
+ \footnote{Isar version by Gertrud Bauer.  Original tactic script by
+ Larry Paulson.  A few proofs of laws taken from
+ \cite{Concrete-Math}.}
+*}
 
-theory Fibonacci = Primes:
 
 subsection {* Fibonacci numbers *}
 
-consts fib :: "nat => nat"
-recdef fib less_than
- "fib 0 = 0"
- "fib (Suc 0) = 1"
- "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+fun fib :: "nat \<Rightarrow> nat" where
+  "fib 0 = 0"
+  | "fib (Suc 0) = 1"
+  | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
 
 lemma [simp]: "0 < fib (Suc n)"
-  by (induct n rule: fib.induct) (simp+)
+  by (induct n rule: fib.induct) simp_all
 
 
 text {* Alternative induction rule. *}
 
 theorem fib_induct:
-  "\<lbrakk>P 0; P 1; \<And>n. \<lbrakk>P (n + 1); P n\<rbrakk> \<Longrightarrow> P (n + 2)\<rbrakk> \<Longrightarrow> P (n::nat)"
-  by (induct rule: fib.induct, simp+)
+    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
+  by (induct rule: fib.induct) simp_all
 
 
 subsection {* Fib and gcd commute *}
@@ -48,102 +70,97 @@ proof (induct n rule: fib_induct)
   finally show "?P (n + 2)" .
 qed
 
-lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
+lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
 proof (induct n rule: fib_induct)
   show "?P 0" by simp
   show "?P 1" by simp
   fix n
   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
     by simp
-  also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
+  also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
     by (simp only: gcd_add2')
-  also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
+  also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
     by (simp add: gcd_commute)
   also assume "... = 1"
   finally show "?P (n + 2)" .
 qed
 
-lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
+lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n"
 proof -
   assume "0 < n"
-  hence "gcd (n * k + m, n) = gcd (n, m mod n)"
+  then have "gcd (n * k + m) n = gcd n (m mod n)"
     by (simp add: gcd_non_0 add_commute)
-  also have "... = gcd (m, n)" by (simp! add: gcd_non_0)
+  also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0)
   finally show ?thesis .
 qed
 
-lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
+lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
 proof (cases m)
-  assume "m = 0"
-  thus ?thesis by simp
+  case 0
+  then show ?thesis by simp
 next
-  fix k assume "m = Suc k"
-  hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
+  case (Suc k)
+  then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
     by (simp add: gcd_commute)
   also have "fib (n + k + 1)
     = fib (k + 1) * fib (n + 1) + fib k * fib n"
     by (rule fib_add)
-  also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
+  also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
     by (simp add: gcd_mult_add)
-  also have "... = gcd (fib n, fib (k + 1))"
+  also have "... = gcd (fib n) (fib (k + 1))"
     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
-  also have "... = gcd (fib m, fib n)"
-    by (simp! add: gcd_commute)
+  also have "... = gcd (fib m) (fib n)"
+    using Suc by (simp add: gcd_commute)
   finally show ?thesis .
 qed
 
 lemma gcd_fib_diff:
-  "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
+  assumes "m <= n"
+  shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
 proof -
-  assume "m <= n"
-  have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
+  have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
     by (simp add: gcd_fib_add)
-  also have "n - m + m = n" by (simp!)
+  also from `m <= n` have "n - m + m = n" by simp
   finally show ?thesis .
 qed
 
 lemma gcd_fib_mod:
-  "0 < m \<Longrightarrow> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
-proof -
-  assume m: "0 < m"
-  show ?thesis
-  proof (induct n rule: nat_less_induct)
-    fix n
-    assume hyp: "ALL ma. ma < n
-      --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)"
-    show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
-    proof -
-      have "n mod m = (if n < m then n else (n - m) mod m)"
-	by (rule mod_if)
-      also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
-      proof cases
-	assume "n < m" thus ?thesis by simp
-      next
-	assume not_lt: "~ n < m" hence le: "m <= n" by simp
-	have "n - m < n" by (simp! add: diff_less)
-	with hyp have "gcd (fib m, fib ((n - m) mod m))
-	  = gcd (fib m, fib (n - m))" by simp
-	also from le have "... = gcd (fib m, fib n)"
-	  by (rule gcd_fib_diff)
-	finally have "gcd (fib m, fib ((n - m) mod m)) =
-	  gcd (fib m, fib n)" .
-	with not_lt show ?thesis by simp
-      qed
-      finally show ?thesis .
+  assumes "0 < m"
+  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+proof (induct n rule: nat_less_induct)
+  case (1 n) note hyp = this
+  show ?case
+  proof -
+    have "n mod m = (if n < m then n else (n - m) mod m)"
+      by (rule mod_if)
+    also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
+    proof (cases "n < m")
+      case True then show ?thesis by simp
+    next
+      case False then have "m <= n" by simp
+      from `0 < m` and False have "n - m < n" by simp
+      with hyp have "gcd (fib m) (fib ((n - m) mod m))
+        = gcd (fib m) (fib (n - m))" by simp
+      also have "... = gcd (fib m) (fib n)"
+        using `m <= n` by (rule gcd_fib_diff)
+      finally have "gcd (fib m) (fib ((n - m) mod m)) =
+        gcd (fib m) (fib n)" .
+      with False show ?thesis by simp
     qed
+    finally show ?thesis .
   qed
 qed
 
 
-theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
+theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
 proof (induct m n rule: gcd_induct)
-  fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
+  fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
   fix n :: nat assume n: "0 < n"
-  hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
-  also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
-  also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
-  also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
-  finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
+  then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0)
+  also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
+  also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
+  also have "... = gcd (fib m) (fib n)" by (rule gcd_commute)
+  finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
 qed
 
 end