--- a/src/HOL/IsaMakefile Thu Jul 01 18:31:46 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 01 19:14:54 2010 +0200
@@ -1012,7 +1012,8 @@
Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \
Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty \
Isar_Examples/document/root.bib Isar_Examples/document/root.tex \
- Isar_Examples/document/style.tex Hoare/hoare_tac.ML
+ Isar_Examples/document/style.tex Hoare/hoare_tac.ML \
+ Number_Theory/Primes.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
--- a/src/HOL/Isar_Examples/Fibonacci.thy Thu Jul 01 18:31:46 2010 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Thu Jul 01 19:14:54 2010 +0200
@@ -15,7 +15,7 @@
header {* Fib and Gcd commute *}
theory Fibonacci
-imports "../Old_Number_Theory/Primes"
+imports "../Number_Theory/Primes"
begin
text_raw {* \footnote{Isar version by Gertrud Bauer. Original tactic
@@ -23,6 +23,9 @@
\cite{Concrete-Math}.} *}
+declare One_nat_def [simp]
+
+
subsection {* Fibonacci numbers *}
fun fib :: "nat \<Rightarrow> nat" where
@@ -30,7 +33,7 @@
| "fib (Suc 0) = 1"
| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
-lemma [simp]: "0 < fib (Suc n)"
+lemma [simp]: "fib (Suc n) > 0"
by (induct n rule: fib.induct) simp_all
@@ -74,20 +77,21 @@
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))"
- by (simp only: gcd_add2')
+ by (rule gcd_add2_nat)
also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
- by (simp add: gcd_commute)
+ by (simp add: gcd_commute_nat)
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::nat) < n ==> 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 add_commute)
- also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0)
+ by (simp add: gcd_non_0_nat add_commute)
+ also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat)
finally show ?thesis .
qed
@@ -98,16 +102,16 @@
next
case (Suc k)
then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
- by (simp add: gcd_commute)
+ by (simp add: gcd_commute_nat)
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))"
by (simp add: gcd_mult_add)
also have "... = gcd (fib n) (fib (k + 1))"
- by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
+ by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat)
also have "... = gcd (fib m) (fib n)"
- using Suc by (simp add: gcd_commute)
+ using Suc by (simp add: gcd_commute_nat)
finally show ?thesis .
qed
@@ -149,13 +153,13 @@
qed
theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
-proof (induct m n rule: gcd_induct)
+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 (rule gcd_non_0)
+ 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)
+ also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat)
finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
qed
--- a/src/HOL/Isar_Examples/ROOT.ML Thu Jul 01 18:31:46 2010 +0200
+++ b/src/HOL/Isar_Examples/ROOT.ML Thu Jul 01 19:14:54 2010 +0200
@@ -1,6 +1,6 @@
(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
-no_document use_thys ["../Old_Number_Theory/Primes", "../Old_Number_Theory/Fibonacci"];
+no_document use_thys ["../Number_Theory/Primes"];
use_thys [
"Basic_Logic",