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.6  
     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.12  
    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.18  
    1.19  lemma pow2_0[simp]: "pow2 0 = 1"
    1.20  by (simp add: pow2_def)
    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.24  
    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.30  
    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.36  
    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.41    by (simp add: float_def)
    1.42  
    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.49  
    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.56  
    1.57  lemma lbound: "lbound x \<le> x"   
    1.58    by (simp add: lbound_def)