author haftmann Thu, 26 Jun 2008 10:06:53 +0200 changeset 27366 d0cda1ea705e parent 27365 91a7041a5a64 child 27367 a75d71c73362
dropped recdef
 src/HOL/Isar_examples/Fibonacci.thy file | annotate | diff | comparison | revisions src/HOL/Real/Float.thy file | annotate | diff | comparison | revisions
```--- 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```
```--- 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 @@
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"```