src/HOL/Number_Theory/Fib.thy
 changeset 53077 a1b3784f8129 parent 44872 a98ef45122f3 child 54713 6666fc0b9ebc
```--- a/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -169,24 +169,24 @@
*}

lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
-    (fib (int n + 1))^2 = (-1)^(n + 1)"
+    (fib (int n + 1))\<^sup>2 = (-1)^(n + 1)"
apply (induct n)
done

lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
-    (fib (n + 1))^2 = (-1)^(nat n + 1)"
+    (fib (n + 1))\<^sup>2 = (-1)^(nat n + 1)"
by (insert fib_Cassini_aux_int [of "nat n"], auto)

(*
lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
-    (fib (n + 1))^2 + (-1)^(nat n + 1)"
+    (fib (n + 1))\<^sup>2 + (-1)^(nat n + 1)"
by (frule fib_Cassini_int, simp)
*)

lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
-  (if even n then tsub ((fib (n + 1))^2) 1
-   else (fib (n + 1))^2 + 1)"
+  (if even n then tsub ((fib (n + 1))\<^sup>2) 1
+   else (fib (n + 1))\<^sup>2 + 1)"
apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
apply (subst tsub_eq)
apply (insert fib_gr_0_int [of "n + 1"], force)
@@ -194,8 +194,8 @@
done

lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
-    (if even n then (fib (n + 1))^2 - 1
-     else (fib (n + 1))^2 + 1)"
+    (if even n then (fib (n + 1))\<^sup>2 - 1
+     else (fib (n + 1))\<^sup>2 + 1)"
by (rule fib_Cassini'_int [transferred, of n], auto)

```