# HG changeset patch
# User wenzelm
# Date 1278004494 -7200
# Node ID 645eb9fec7940d1db4ce035168a5182f7850890d
# Parent  fa53d267dab348a15b3074d215bbdf1521738ba3
avoid Old_Number_Theory;
more precise dependencies;

diff -r fa53d267dab3 -r 645eb9fec794 src/HOL/IsaMakefile
--- 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
 
 
diff -r fa53d267dab3 -r 645eb9fec794 src/HOL/Isar_Examples/Fibonacci.thy
--- 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
 
diff -r fa53d267dab3 -r 645eb9fec794 src/HOL/Isar_Examples/ROOT.ML
--- 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",