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.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.70 +  pred_Pls pred_Min pred_1 pred_0
1.71 +  succ_Pls succ_Min succ_1 succ_0
1.73 +  add_BIT_11 minus_Pls minus_Min minus_1
1.74 +  minus_0 mult_Pls mult_Min mult_num1 mult_num0
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
```