# HG changeset patch
# User wenzelm
# Date 1463248783 -7200
# Node ID 201480e65b7d2a717bdb36d28c2f54c6a063051b
# Parent  056ea294c256a7d8b8d702a356736b4c5eb5fe93
tuned;

diff -r 056ea294c256 -r 201480e65b7d src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Sat May 14 19:49:10 2016 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Sat May 14 19:59:43 2016 +0200
@@ -27,7 +27,8 @@
 
 subsection \<open>Fibonacci numbers\<close>
 
-fun fib :: "nat \<Rightarrow> nat" where
+fun fib :: "nat \<Rightarrow> nat"
+where
   "fib 0 = 0"
 | "fib (Suc 0) = 1"
 | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
@@ -38,9 +39,8 @@
 
 text \<open>Alternative induction rule.\<close>
 
-theorem fib_induct:
-  fixes n :: nat
-  shows "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
+theorem fib_induct: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
+  for n :: nat
   by (induct rule: fib.induct) simp_all
 
 
@@ -48,8 +48,7 @@
 
 text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>
 
-lemma fib_add:
-  "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
+lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
   (is "?P n")
   \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
 proof (induct n rule: fib_induct)
@@ -58,19 +57,16 @@
   fix n
   have "fib (n + 2 + k + 1)
     = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp
-  also assume "fib (n + k + 1)
-    = fib (k + 1) * fib (n + 1) + fib k * fib n"
-      (is " _ = ?R1")
-  also assume "fib (n + 1 + k + 1)
-    = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
-      (is " _ = ?R2")
-  also have "?R1 + ?R2
-    = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
+  also assume "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" (is " _ = ?R1")
+  also assume "fib (n + 1 + k + 1) = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)"
+    (is " _ = ?R2")
+  also have "?R1 + ?R2 = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)"
     by (simp add: add_mult_distrib2)
   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
@@ -105,8 +101,7 @@
   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"
+  also have "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
     by (rule fib_add)
   also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
     by (simp add: gcd_mult_add)
@@ -117,9 +112,7 @@
   finally show ?thesis .
 qed
 
-lemma gcd_fib_diff:
-  assumes "m \<le> n"
-  shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
+lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" if "m \<le> n"
 proof -
   have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
     by (simp add: gcd_fib_add)
@@ -128,11 +121,9 @@
   finally show ?thesis .
 qed
 
-lemma gcd_fib_mod:
-  assumes "0 < m"
-  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" if "0 < m"
 proof (induct n rule: nat_less_induct)
-  case (1 n) note hyp = this
+  case hyp: (1 n)
   show ?case
   proof -
     have "n mod m = (if n < m then n else (n - m) mod m)"
@@ -158,12 +149,12 @@
   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_nat_induct)
-  fix m
+  fix m n :: nat
   show "fib (gcd m 0) = gcd (fib m) (fib 0)"
     by simp
-  fix n :: nat
   assume n: "0 < n"
   then have "gcd m n = gcd n (m mod n)"
     by (simp add: gcd_non_0_nat)