# HG changeset patch
# User haftmann
# Date 1214467613 -7200
# Node ID d0cda1ea705e3625aa8f8e29d16e3d05b099d8d7
# Parent  91a7041a5a6416e7fe8df2ca7aec112255f1f580
dropped recdef

diff -r 91a7041a5a64 -r d0cda1ea705e src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Thu Jun 26 10:06:51 2008 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Thu Jun 26 10:06:53 2008 +0200
@@ -15,7 +15,9 @@
 
 header {* Fib and Gcd commute *}
 
-theory Fibonacci imports Primes begin
+theory Fibonacci
+imports Primes
+begin
 
 text_raw {*
  \footnote{Isar version by Gertrud Bauer.  Original tactic script by
@@ -26,11 +28,10 @@
 
 subsection {* Fibonacci numbers *}
 
-consts fib :: "nat => nat"
-recdef fib less_than
+fun fib :: "nat \<Rightarrow> nat" where
   "fib 0 = 0"
-  "fib (Suc 0) = 1"
-  "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+  | "fib (Suc 0) = 1"
+  | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
 
 lemma [simp]: "0 < fib (Suc n)"
   by (induct n rule: fib.induct) simp_all
diff -r 91a7041a5a64 -r d0cda1ea705e src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Thu Jun 26 10:06:51 2008 +0200
+++ b/src/HOL/Real/Float.thy	Thu Jun 26 10:06:53 2008 +0200
@@ -264,9 +264,6 @@
     by (simp add: a)
 qed
 
-consts
-  norm_float :: "int*int \<Rightarrow> int*int"
-
 lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
 by (rule zdiv_int)
 
@@ -276,29 +273,25 @@
 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
 by arith
 
-lemma terminating_norm_float: "\<forall>a. (a::int) \<noteq> 0 \<and> even a \<longrightarrow> a \<noteq> 0 \<and> \<bar>a div 2\<bar> < \<bar>a\<bar>"
-apply (auto)
-apply (rule abs_div_2_less)
-apply (auto)
-done
+function norm_float :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
+  "norm_float a b = (if a \<noteq> 0 \<and> even a then norm_float (a div 2) (b + 1)
+    else if a = 0 then (0, 0) else (a, b))"
+by auto
 
-declare [[simp_depth_limit = 2]]
-recdef norm_float "measure (% (a,b). nat (abs a))"
-  "norm_float (a,b) = (if (a \<noteq> 0) & (even a) then norm_float (a div 2, b+1) else (if a=0 then (0,0) else (a,b)))"
-(hints simp: even_def terminating_norm_float)
-declare [[simp_depth_limit = 100]]
+termination by (relation "measure (nat o abs o fst)")
+  (auto intro: abs_div_2_less)
 
-lemma norm_float: "float x = float (norm_float x)"
+lemma norm_float: "float x = float (split norm_float x)"
 proof -
   {
     fix a b :: int
-    have norm_float_pair: "float (a,b) = float (norm_float (a,b))"
+    have norm_float_pair: "float (a, b) = float (norm_float a b)"
     proof (induct a b rule: norm_float.induct)
       case (1 u v)
       show ?case
       proof cases
         assume u: "u \<noteq> 0 \<and> even u"
-        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2, v + 1))" by auto
+        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
         with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
         then show ?thesis
           apply (subst norm_float.simps)
@@ -314,7 +307,7 @@
   note helper = this
   have "? a b. x = (a,b)" by auto
   then obtain a b where "x = (a, b)" by blast
-  then show ?thesis by (simp only: helper)
+  then show ?thesis by (simp add: helper)
 qed
 
 lemma float_add_l0: "float (0, e) + x = x"