src/HOL/Real/Float.thy
changeset 20485 3078fd2eec7b
parent 20217 25b068a99d2b
child 20717 2244b0d719a0
     1.1 --- a/src/HOL/Real/Float.thy	Wed Sep 06 10:01:27 2006 +0200
     1.2 +++ b/src/HOL/Real/Float.thy	Wed Sep 06 13:48:02 2006 +0200
     1.3 @@ -3,7 +3,9 @@
     1.4      Author: Steven Obua
     1.5  *)
     1.6  
     1.7 -theory Float imports Real begin
     1.8 +theory Float
     1.9 +imports Real
    1.10 +begin
    1.11  
    1.12  definition
    1.13    pow2 :: "int \<Rightarrow> real"
    1.14 @@ -177,7 +179,7 @@
    1.15    ultimately show ?thesis by auto
    1.16  qed
    1.17  
    1.18 -lemma real_is_int_number_of[simp]: "real_is_int ((number_of::bin\<Rightarrow>real) x)"
    1.19 +lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
    1.20  proof -
    1.21    have neg1: "real_is_int (-1::real)"
    1.22    proof -
    1.23 @@ -187,11 +189,9 @@
    1.24    qed
    1.25  
    1.26    {
    1.27 -    fix x::int
    1.28 -    have "!! y. real_is_int ((number_of::bin\<Rightarrow>real) (Abs_Bin x))"
    1.29 -      apply (simp add: number_of_eq)
    1.30 -      apply (subst Abs_Bin_inverse)
    1.31 -      apply (simp add: Bin_def)
    1.32 +    fix x :: int
    1.33 +    have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
    1.34 +      unfolding number_of_eq
    1.35        apply (induct x)
    1.36        apply (induct_tac n)
    1.37        apply (simp)
    1.38 @@ -212,13 +212,13 @@
    1.39    }
    1.40    note Abs_Bin = this
    1.41    {
    1.42 -    fix x :: bin
    1.43 -    have "? u. x = Abs_Bin u"
    1.44 -      apply (rule exI[where x = "Rep_Bin x"])
    1.45 -      apply (simp add: Rep_Bin_inverse)
    1.46 +    fix x :: int
    1.47 +    have "? u. x = u"
    1.48 +      apply (rule exI[where x = "x"])
    1.49 +      apply (simp)
    1.50        done
    1.51    }
    1.52 -  then obtain u::int where "x = Abs_Bin u" by auto
    1.53 +  then obtain u::int where "x = u" by auto
    1.54    with Abs_Bin show ?thesis by auto
    1.55  qed
    1.56  
    1.57 @@ -448,17 +448,17 @@
    1.58  
    1.59  lemma not_true_eq_false: "(~ True) = False" by simp
    1.60  
    1.61 -
    1.62  lemmas binarith =
    1.63    Pls_0_eq Min_1_eq
    1.64 -  bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
    1.65 -  bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
    1.66 -  bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10
    1.67 -  bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
    1.68 -  bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
    1.69 -  bin_add_Pls_right bin_add_Min_right
    1.70 +  pred_Pls pred_Min pred_1 pred_0
    1.71 +  succ_Pls succ_Min succ_1 succ_0
    1.72 +  add_Pls add_Min add_BIT_0 add_BIT_10
    1.73 +  add_BIT_11 minus_Pls minus_Min minus_1
    1.74 +  minus_0 mult_Pls mult_Min mult_num1 mult_num0
    1.75 +  add_Pls_right add_Min_right
    1.76  
    1.77 -lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
    1.78 +lemma int_eq_number_of_eq:
    1.79 +  "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
    1.80    by simp
    1.81  
    1.82  lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
    1.83 @@ -473,7 +473,7 @@
    1.84  lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
    1.85    by simp
    1.86  
    1.87 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
    1.88 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
    1.89    by simp
    1.90  
    1.91  lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
    1.92 @@ -485,7 +485,7 @@
    1.93  lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
    1.94    by simp
    1.95  
    1.96 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
    1.97 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
    1.98    by simp
    1.99  
   1.100  lemmas intarithrel =
   1.101 @@ -494,16 +494,16 @@
   1.102    lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
   1.103    int_neg_number_of_BIT int_le_number_of_eq
   1.104  
   1.105 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
   1.106 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   1.107    by simp
   1.108  
   1.109 -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
   1.110 +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   1.111    by simp
   1.112  
   1.113 -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
   1.114 +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
   1.115    by simp
   1.116  
   1.117 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
   1.118 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   1.119    by simp
   1.120  
   1.121  lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym