src/HOL/Isar_Examples/Fibonacci.thy

--- a/src/HOL/Isar_Examples/Fibonacci.thy	Thu Feb 20 23:16:33 2014 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Thu Feb 20 23:46:40 2014 +0100
@@ -40,7 +40,8 @@
 text {* Alternative induction rule. *}
 
 theorem fib_induct:
-    "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)"
+  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"
   by (induct rule: fib.induct) simp_all
 
 
@@ -77,21 +78,23 @@
   fix n
   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
     by simp
-  also have "... = fib (n + 2) + fib (n + 1)" by simp
-  also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
+  also have "\<dots> = fib (n + 2) + fib (n + 1)"
+    by simp
+  also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
     by (rule gcd_add2_nat)
-  also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
+  also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
     by (simp add: gcd_commute_nat)
-  also assume "... = 1"
+  also assume "\<dots> = 1"
   finally show "?P (n + 2)" .
 qed
 
-lemma gcd_mult_add: "(0::nat) < n ==> gcd (n * k + m) n = gcd m n"
+lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
 proof -
   assume "0 < n"
   then have "gcd (n * k + m) n = gcd n (m mod n)"
     by (simp add: gcd_non_0_nat add_commute)
-  also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat)
+  also from `0 < n` have "\<dots> = gcd m n"
+    by (simp add: gcd_non_0_nat)
   finally show ?thesis .
 qed
 
@@ -106,22 +109,23 @@
   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 \<dots> (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 "\<dots> = gcd (fib n) (fib (k + 1))"
     by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
-  also have "... = gcd (fib m) (fib n)"
+  also have "\<dots> = gcd (fib m) (fib n)"
     using Suc by (simp add: gcd_commute_nat)
   finally show ?thesis .
 qed
 
 lemma gcd_fib_diff:
-  assumes "m <= n"
+  assumes "m \<le> n"
   shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
 proof -
   have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
     by (simp add: gcd_fib_add)
-  also from `m <= n` have "n - m + m = n" by simp
+  also from `m \<le> n` have "n - m + m = n"
+    by simp
   finally show ?thesis .
 qed
 
@@ -134,15 +138,18 @@
   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)"
+    also have "gcd (fib m) (fib \<dots>) = gcd (fib m) (fib n)"
     proof (cases "n < m")
-      case True then show ?thesis by simp
+      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
+      case False
+      then have "m \<le> 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)"
+      also have "\<dots> = 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)" .
@@ -154,12 +161,18 @@
 
 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 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)
-  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_nat)
+  fix m
+  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)
+  also assume hyp: "fib \<dots> = gcd (fib n) (fib (m mod n))"
+  also from n have "\<dots> = gcd (fib n) (fib m)"
+    by (rule gcd_fib_mod)
+  also have "\<dots> = gcd (fib m) (fib n)"
+    by (rule gcd_commute_nat)
   finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
 qed