src/HOL/Matrix/ComputeFloat.thy
 changeset 38273 d31a34569542 parent 35032 7efe662e41b4 child 41413 64cd30d6b0b8
1.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Wed Aug 11 00:47:09 2010 +0200
1.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Wed Aug 11 12:40:08 2010 +0200
1.3 @@ -9,13 +9,11 @@
1.4  uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
1.5  begin
1.7 -definition
1.8 -  pow2 :: "int \<Rightarrow> real" where
1.9 -  "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
1.10 +definition pow2 :: "int \<Rightarrow> real"
1.11 +  where "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
1.13 -definition
1.14 -  float :: "int * int \<Rightarrow> real" where
1.15 -  "float x = real (fst x) * pow2 (snd x)"
1.16 +definition float :: "int * int \<Rightarrow> real"
1.17 +  where "float x = real (fst x) * pow2 (snd x)"
1.19  lemma pow2_0[simp]: "pow2 0 = 1"
1.21 @@ -99,13 +97,11 @@
1.22  lemma "float (a, e) + float (b, e) = float (a + b, e)"
1.23  by (simp add: float_def algebra_simps)
1.25 -definition
1.26 -  int_of_real :: "real \<Rightarrow> int" where
1.27 -  "int_of_real x = (SOME y. real y = x)"
1.28 +definition int_of_real :: "real \<Rightarrow> int"
1.29 +  where "int_of_real x = (SOME y. real y = x)"
1.31 -definition
1.32 -  real_is_int :: "real \<Rightarrow> bool" where
1.33 -  "real_is_int x = (EX (u::int). x = real u)"
1.34 +definition real_is_int :: "real \<Rightarrow> bool"
1.35 +  where "real_is_int x = (EX (u::int). x = real u)"
1.37  lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
1.38  by (auto simp add: real_is_int_def int_of_real_def)
1.39 @@ -345,15 +341,11 @@
1.40  lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
1.43 -definition
1.44 -  lbound :: "real \<Rightarrow> real"
1.45 -where
1.46 -  "lbound x = min 0 x"
1.47 +definition lbound :: "real \<Rightarrow> real"
1.48 +  where "lbound x = min 0 x"
1.50 -definition
1.51 -  ubound :: "real \<Rightarrow> real"
1.52 -where
1.53 -  "ubound x = max 0 x"
1.54 +definition ubound :: "real \<Rightarrow> real"
1.55 +  where "ubound x = max 0 x"
1.57  lemma lbound: "lbound x \<le> x"