1.1 --- a/src/HOL/Complex/CLim.thy Wed Jun 30 14:04:58 2004 +0200
1.2 +++ b/src/HOL/Complex/CLim.thy Thu Jul 01 12:29:53 2004 +0200
1.3 @@ -666,8 +666,8 @@
1.4 apply (subgoal_tac "xa + - (hcomplex_of_complex x) \<noteq> 0")
1.5 prefer 2 apply (simp add: compare_rls)
1.6 apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec)
1.7 - prefer 2 apply (simp add: hcomplex_add_assoc [symmetric])
1.8 -apply (auto simp add: mem_cinfmal_iff [symmetric] hcomplex_add_commute)
1.9 + prefer 2 apply (simp add: add_assoc [symmetric])
1.10 +apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute)
1.11 apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1)
1.12 apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
1.13 simp add: mult_assoc)
1.14 @@ -740,7 +740,7 @@
1.15 CInfinitesimal_add CInfinitesimal_mult
1.16 CInfinitesimal_hcomplex_of_complex_mult
1.17 CInfinitesimal_hcomplex_of_complex_mult2
1.18 - simp add: hcomplex_add_assoc [symmetric])
1.19 + simp add: add_assoc [symmetric])
1.20 done
1.21
1.22 lemma CDERIV_mult:
1.23 @@ -899,7 +899,7 @@
1.24 "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
1.25 apply (induct_tac "n")
1.26 apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult])
1.27 -apply (auto simp add: complex_of_real_add [symmetric] left_distrib real_of_nat_Suc)
1.28 +apply (auto simp add: left_distrib real_of_nat_Suc)
1.29 apply (case_tac "n")
1.30 apply (auto simp add: mult_ac add_commute)
1.31 done
1.32 @@ -930,7 +930,8 @@
1.33 apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add
1.34 inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
1.35 add_ac mult_ac
1.36 - del: inverse_minus_eq inverse_mult_distrib minus_mult_right [symmetric] minus_mult_left [symmetric])
1.37 + del: inverse_minus_eq inverse_mult_distrib
1.38 + minus_mult_right [symmetric] minus_mult_left [symmetric])
1.39 apply (simp only: mult_assoc [symmetric] right_distrib)
1.40 apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans)
1.41 apply (rule inverse_add_CInfinitesimal_capprox2)
1.42 @@ -952,7 +953,8 @@
1.43 "[| CDERIV f x :> d; f(x) \<noteq> 0 |]
1.44 ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
1.45 apply (rule mult_commute [THEN subst])
1.46 -apply (simp (no_asm_simp) add: minus_mult_left power_inverse del: complexpow_Suc minus_mult_left [symmetric])
1.47 +apply (simp add: minus_mult_left power_inverse
1.48 + del: complexpow_Suc minus_mult_left [symmetric])
1.49 apply (fold o_def)
1.50 apply (blast intro!: CDERIV_chain CDERIV_inverse)
1.51 done
2.1 --- a/src/HOL/Complex/CSeries.thy Wed Jun 30 14:04:58 2004 +0200
2.2 +++ b/src/HOL/Complex/CSeries.thy Thu Jul 01 12:29:53 2004 +0200
2.3 @@ -72,7 +72,7 @@
2.4
2.5 lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
2.6 apply (induct_tac "n")
2.7 -apply (auto simp add: left_distrib complex_of_real_add [symmetric] real_of_nat_Suc)
2.8 +apply (auto simp add: left_distrib real_of_nat_Suc)
2.9 done
2.10
2.11 lemma sumc_add_mult_const:
2.12 @@ -98,16 +98,16 @@
2.13
2.14 lemma sumc_interval_const [rule_format (no_asm)]:
2.15 "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
2.16 - --> sumc m na f = (complex_of_real(real (na - m)) * r)"
2.17 + --> sumc m na f = (complex_of_real(real (na - m)) * r)"
2.18 apply (induct_tac "na")
2.19 -apply (auto simp add: Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric] left_distrib)
2.20 +apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
2.21 done
2.22
2.23 lemma sumc_interval_const2 [rule_format (no_asm)]:
2.24 "(\<forall>n. m \<le> n --> f n = r) & m \<le> na
2.25 --> sumc m na f = (complex_of_real(real (na - m)) * r)"
2.26 apply (induct_tac "na")
2.27 -apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric])
2.28 +apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
2.29 done
2.30
2.31 (***
3.1 --- a/src/HOL/Complex/Complex.thy Wed Jun 30 14:04:58 2004 +0200
3.2 +++ b/src/HOL/Complex/Complex.thy Thu Jul 01 12:29:53 2004 +0200
3.3 @@ -291,35 +291,33 @@
3.4 "(complex_of_real x = complex_of_real y) = (x = y)"
3.5 by (simp add: complex_of_real_def)
3.6
3.7 -lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"
3.8 +lemma complex_of_real_minus [simp]: "complex_of_real(-x) = - complex_of_real x"
3.9 by (simp add: complex_of_real_def complex_minus)
3.10
3.11 -lemma complex_of_real_inverse:
3.12 +lemma complex_of_real_inverse [simp]:
3.13 "complex_of_real(inverse x) = inverse(complex_of_real x)"
3.14 apply (case_tac "x=0", simp)
3.15 -apply (simp add: complex_inverse complex_of_real_def real_divide_def
3.16 - inverse_mult_distrib power2_eq_square)
3.17 +apply (simp add: complex_of_real_def divide_inverse power2_eq_square)
3.18 done
3.19
3.20 -lemma complex_of_real_add:
3.21 - "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
3.22 +lemma complex_of_real_add [simp]:
3.23 + "complex_of_real (x + y) = complex_of_real x + complex_of_real y"
3.24 by (simp add: complex_add complex_of_real_def)
3.25
3.26 -lemma complex_of_real_diff:
3.27 - "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
3.28 -by (simp add: complex_of_real_minus [symmetric] complex_diff_def
3.29 - complex_of_real_add)
3.30 +lemma complex_of_real_diff [simp]:
3.31 + "complex_of_real (x - y) = complex_of_real x - complex_of_real y"
3.32 +by (simp add: complex_of_real_minus diff_minus)
3.33
3.34 -lemma complex_of_real_mult:
3.35 - "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
3.36 +lemma complex_of_real_mult [simp]:
3.37 + "complex_of_real (x * y) = complex_of_real x * complex_of_real y"
3.38 by (simp add: complex_mult complex_of_real_def)
3.39
3.40 -lemma complex_of_real_divide:
3.41 - "complex_of_real x / complex_of_real y = complex_of_real(x/y)"
3.42 +lemma complex_of_real_divide [simp]:
3.43 + "complex_of_real(x/y) = complex_of_real x / complex_of_real y"
3.44 apply (simp add: complex_divide_def)
3.45 apply (case_tac "y=0", simp)
3.46 -apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse
3.47 - real_divide_def)
3.48 +apply (simp add: complex_of_real_mult complex_of_real_inverse
3.49 + divide_inverse)
3.50 done
3.51
3.52 lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
3.53 @@ -407,7 +405,7 @@
3.54 by (induct w, induct z, simp add: complex_cnj complex_add)
3.55
3.56 lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
3.57 -by (simp add: complex_diff_def complex_cnj_add complex_cnj_minus)
3.58 +by (simp add: diff_minus complex_cnj_add complex_cnj_minus)
3.59
3.60 lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
3.61 by (induct w, induct z, simp add: complex_cnj complex_mult)
3.62 @@ -423,7 +421,7 @@
3.63
3.64 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
3.65 apply (induct z)
3.66 -apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def
3.67 +apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus
3.68 complex_minus i_def complex_mult)
3.69 done
3.70
3.71 @@ -561,7 +559,7 @@
3.72 done
3.73
3.74 lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
3.75 -by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse)
3.76 +by (simp add: complex_divide_def divide_inverse complex_mod_mult complex_mod_inverse)
3.77
3.78
3.79 subsection{*Exponentiation*}
3.80 @@ -639,24 +637,33 @@
3.81 lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
3.82 by (simp add: i_def)
3.83
3.84 +
3.85 +
3.86 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
3.87 -apply (induct z)
3.88 -apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
3.89 -apply (simp add: complex_of_real_def complex_mult real_divide_def)
3.90 -done
3.91 +proof (induct z)
3.92 + case (Complex x y)
3.93 + have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
3.94 + by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
3.95 + thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)"
3.96 + by (simp add: sgn_def complex_of_real_def divide_inverse)
3.97 +qed
3.98 +
3.99
3.100 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
3.101 -apply (induct z)
3.102 -apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
3.103 -apply (simp add: complex_of_real_def complex_mult real_divide_def)
3.104 -done
3.105 +proof (induct z)
3.106 + case (Complex x y)
3.107 + have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
3.108 + by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
3.109 + thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)"
3.110 + by (simp add: sgn_def complex_of_real_def divide_inverse)
3.111 +qed
3.112
3.113 lemma complex_inverse_complex_split:
3.114 "inverse(complex_of_real x + ii * complex_of_real y) =
3.115 complex_of_real(x/(x ^ 2 + y ^ 2)) -
3.116 ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
3.117 by (simp add: complex_of_real_def i_def complex_mult complex_add
3.118 - complex_diff_def complex_minus complex_inverse real_divide_def)
3.119 + diff_minus complex_minus complex_inverse divide_inverse)
3.120
3.121 (*----------------------------------------------------------------------------*)
3.122 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
3.123 @@ -738,7 +745,8 @@
3.124 by (simp add: rcis_def)
3.125
3.126 lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
3.127 -by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib)
3.128 +by (simp add: rcis_def cis_def cos_add sin_add right_distrib right_diff_distrib
3.129 + complex_of_real_def)
3.130
3.131 lemma cis_mult: "cis a * cis b = cis (a + b)"
3.132 by (simp add: cis_rcis_eq rcis_mult)
3.133 @@ -774,7 +782,7 @@
3.134
3.135 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
3.136 by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus
3.137 - complex_diff_def)
3.138 + diff_minus)
3.139
3.140 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
3.141 by (simp add: divide_inverse rcis_def complex_of_real_inverse)
3.142 @@ -818,33 +826,31 @@
3.143
3.144 instance complex :: number ..
3.145
3.146 -primrec (*the type constraint is essential!*)
3.147 - number_of_Pls: "number_of bin.Pls = 0"
3.148 - number_of_Min: "number_of bin.Min = - (1::complex)"
3.149 - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
3.150 - (number_of w) + (number_of w)"
3.151 -
3.152 -declare number_of_Pls [simp del]
3.153 - number_of_Min [simp del]
3.154 - number_of_BIT [simp del]
3.155 +defs (overloaded)
3.156 + complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
3.157 + --{*the type constraint is essential!*}
3.158
3.159 instance complex :: number_ring
3.160 -proof
3.161 - show "Numeral0 = (0::complex)" by (rule number_of_Pls)
3.162 - show "-1 = - (1::complex)" by (rule number_of_Min)
3.163 - fix w :: bin and x :: bool
3.164 - show "(number_of (w BIT x) :: complex) =
3.165 - (if x then 1 else 0) + number_of w + number_of w"
3.166 - by (rule number_of_BIT)
3.167 +by (intro_classes, simp add: complex_number_of_def)
3.168 +
3.169 +
3.170 +lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n"
3.171 +by (induct n, simp_all)
3.172 +
3.173 +lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z"
3.174 +proof (cases z)
3.175 + case (1 n)
3.176 + thus ?thesis by simp
3.177 +next
3.178 + case (2 n)
3.179 + thus ?thesis
3.180 + by (simp only: of_int_minus complex_of_real_minus, simp)
3.181 qed
3.182
3.183
3.184 text{*Collapse applications of @{term complex_of_real} to @{term number_of}*}
3.185 lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
3.186 -apply (induct w)
3.187 -apply (simp_all only: number_of complex_of_real_add [symmetric]
3.188 - complex_of_real_minus, simp_all)
3.189 -done
3.190 +by (simp add: complex_number_of_def real_number_of_def)
3.191
3.192 text{*This theorem is necessary because theorems such as
3.193 @{text iszero_number_of_0} only hold for ordered rings. They cannot
3.194 @@ -855,50 +861,6 @@
3.195 by (simp only: complex_of_real_zero_iff complex_number_of [symmetric]
3.196 iszero_def)
3.197
3.198 -
3.199 -(*These allow simplification of expressions involving mixed numbers.
3.200 - Convert???
3.201 -Goalw [complex_number_of_def]
3.202 - "((number_of xa :: complex) + ii * number_of ya =
3.203 - number_of xb) =
3.204 - (((number_of xa :: complex) = number_of xb) &
3.205 - ((number_of ya :: complex) = 0))"
3.206 -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2,
3.207 - complex_of_real_zero_iff]));
3.208 -qed "complex_number_of_eq_cancel_iff2";
3.209 -Addsimps [complex_number_of_eq_cancel_iff2];
3.210 -
3.211 -Goalw [complex_number_of_def]
3.212 - "((number_of xa :: complex) + number_of ya * ii = \
3.213 -\ number_of xb) = \
3.214 -\ (((number_of xa :: complex) = number_of xb) & \
3.215 -\ ((number_of ya :: complex) = 0))";
3.216 -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2a,
3.217 - complex_of_real_zero_iff]));
3.218 -qed "complex_number_of_eq_cancel_iff2a";
3.219 -Addsimps [complex_number_of_eq_cancel_iff2a];
3.220 -
3.221 -Goalw [complex_number_of_def]
3.222 - "((number_of xa :: complex) + ii * number_of ya = \
3.223 -\ ii * number_of yb) = \
3.224 -\ (((number_of xa :: complex) = 0) & \
3.225 -\ ((number_of ya :: complex) = number_of yb))";
3.226 -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3,
3.227 - complex_of_real_zero_iff]));
3.228 -qed "complex_number_of_eq_cancel_iff3";
3.229 -Addsimps [complex_number_of_eq_cancel_iff3];
3.230 -
3.231 -Goalw [complex_number_of_def]
3.232 - "((number_of xa :: complex) + number_of ya * ii= \
3.233 -\ ii * number_of yb) = \
3.234 -\ (((number_of xa :: complex) = 0) & \
3.235 -\ ((number_of ya :: complex) = number_of yb))";
3.236 -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3a,
3.237 - complex_of_real_zero_iff]));
3.238 -qed "complex_number_of_eq_cancel_iff3a";
3.239 -Addsimps [complex_number_of_eq_cancel_iff3a];
3.240 -*)
3.241 -
3.242 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
3.243 apply (subst complex_number_of [symmetric])
3.244 apply (rule complex_cnj_complex_of_real)
3.245 @@ -957,7 +919,6 @@
3.246 val complex_zero_def = thm"complex_zero_def";
3.247 val complex_one_def = thm"complex_one_def";
3.248 val complex_minus_def = thm"complex_minus_def";
3.249 -val complex_diff_def = thm"complex_diff_def";
3.250 val complex_divide_def = thm"complex_divide_def";
3.251 val complex_mult_def = thm"complex_mult_def";
3.252 val complex_add_def = thm"complex_add_def";
4.1 --- a/src/HOL/Complex/NSCA.thy Wed Jun 30 14:04:58 2004 +0200
4.2 +++ b/src/HOL/Complex/NSCA.thy Thu Jul 01 12:29:53 2004 +0200
4.3 @@ -508,7 +508,7 @@
4.4 lemma capprox_SComplex_mult_cancel_zero:
4.5 "[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0"
4.6 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
4.7 -apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
4.8 +apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
4.9 done
4.10
4.11 lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
4.12 @@ -524,7 +524,7 @@
4.13 lemma capprox_SComplex_mult_cancel:
4.14 "[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z"
4.15 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
4.16 -apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
4.17 +apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
4.18 done
4.19
4.20 lemma capprox_SComplex_mult_cancel_iff1 [simp]:
4.21 @@ -618,7 +618,7 @@
4.22 lemma CInfinitesimal_ratio:
4.23 "[| y \<noteq> 0; y \<in> CInfinitesimal; x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
4.24 apply (drule CInfinitesimal_CFinite_mult2, assumption)
4.25 -apply (simp add: divide_inverse hcomplex_mult_assoc)
4.26 +apply (simp add: divide_inverse mult_assoc)
4.27 done
4.28
4.29 lemma SComplex_capprox_iff:
4.30 @@ -901,10 +901,11 @@
4.31 apply (drule CFinite_inverse2)+
4.32 apply (drule capprox_mult2, assumption, auto)
4.33 apply (drule_tac c = "inverse x" in capprox_mult1, assumption)
4.34 -apply (auto intro: capprox_sym simp add: hcomplex_mult_assoc)
4.35 +apply (auto intro: capprox_sym simp add: mult_assoc)
4.36 done
4.37
4.38 -lemmas hcomplex_of_complex_capprox_inverse = hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
4.39 +lemmas hcomplex_of_complex_capprox_inverse =
4.40 + hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
4.41
4.42 lemma inverse_add_CInfinitesimal_capprox:
4.43 "[| x \<in> CFinite - CInfinitesimal;
4.44 @@ -935,7 +936,7 @@
4.45 apply safe
4.46 apply (frule CFinite_inverse, assumption)
4.47 apply (drule not_CInfinitesimal_not_zero)
4.48 -apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
4.49 +apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
4.50 done
4.51
4.52 lemma capprox_CFinite_mult_cancel_iff1:
5.1 --- a/src/HOL/Complex/NSComplex.thy Wed Jun 30 14:04:58 2004 +0200
5.2 +++ b/src/HOL/Complex/NSComplex.thy Thu Jul 01 12:29:53 2004 +0200
5.3 @@ -475,51 +475,48 @@
5.4 apply (simp add: hcomplex_of_hypreal)
5.5 done
5.6
5.7 -lemma hcomplex_of_hypreal_minus:
5.8 - "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
5.9 -apply (cases x)
5.10 -apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
5.11 -done
5.12 -
5.13 -lemma hcomplex_of_hypreal_inverse:
5.14 - "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
5.15 -apply (cases x)
5.16 -apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
5.17 -done
5.18 -
5.19 -lemma hcomplex_of_hypreal_add:
5.20 - "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
5.21 - hcomplex_of_hypreal (x + y)"
5.22 -apply (cases x, cases y)
5.23 -apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
5.24 -done
5.25 -
5.26 -lemma hcomplex_of_hypreal_diff:
5.27 - "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
5.28 - hcomplex_of_hypreal (x - y)"
5.29 -by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
5.30 -
5.31 -lemma hcomplex_of_hypreal_mult:
5.32 - "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
5.33 - hcomplex_of_hypreal (x * y)"
5.34 -apply (cases x, cases y)
5.35 -apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
5.36 -done
5.37 -
5.38 -lemma hcomplex_of_hypreal_divide:
5.39 - "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
5.40 -apply (simp add: hcomplex_divide_def)
5.41 -apply (case_tac "y=0", simp)
5.42 -apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
5.43 -apply (simp add: hypreal_divide_def)
5.44 -done
5.45 -
5.46 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
5.47 by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num)
5.48
5.49 lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
5.50 by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
5.51
5.52 +lemma hcomplex_of_hypreal_minus [simp]:
5.53 + "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
5.54 +apply (cases x)
5.55 +apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus)
5.56 +done
5.57 +
5.58 +lemma hcomplex_of_hypreal_inverse [simp]:
5.59 + "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
5.60 +apply (cases x)
5.61 +apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse)
5.62 +done
5.63 +
5.64 +lemma hcomplex_of_hypreal_add [simp]:
5.65 + "hcomplex_of_hypreal (x + y) = hcomplex_of_hypreal x + hcomplex_of_hypreal y"
5.66 +apply (cases x, cases y)
5.67 +apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add)
5.68 +done
5.69 +
5.70 +lemma hcomplex_of_hypreal_diff [simp]:
5.71 + "hcomplex_of_hypreal (x - y) =
5.72 + hcomplex_of_hypreal x - hcomplex_of_hypreal y "
5.73 +by (simp add: hcomplex_diff_def hypreal_diff_def)
5.74 +
5.75 +lemma hcomplex_of_hypreal_mult [simp]:
5.76 + "hcomplex_of_hypreal (x * y) = hcomplex_of_hypreal x * hcomplex_of_hypreal y"
5.77 +apply (cases x, cases y)
5.78 +apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult)
5.79 +done
5.80 +
5.81 +lemma hcomplex_of_hypreal_divide [simp]:
5.82 + "hcomplex_of_hypreal(x/y) = hcomplex_of_hypreal x / hcomplex_of_hypreal y"
5.83 +apply (simp add: hcomplex_divide_def)
5.84 +apply (case_tac "y=0", simp)
5.85 +apply (simp add: hypreal_divide_def)
5.86 +done
5.87 +
5.88 lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
5.89 apply (cases z)
5.90 apply (auto simp add: hcomplex_of_hypreal hRe)
5.91 @@ -599,7 +596,7 @@
5.92
5.93 lemma HComplex_add [simp]:
5.94 "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
5.95 -by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib)
5.96 +by (simp add: HComplex_def add_ac right_distrib)
5.97
5.98 lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
5.99 by (simp add: HComplex_def hcomplex_of_hypreal_minus)
5.100 @@ -611,7 +608,6 @@
5.101 lemma HComplex_mult [simp]:
5.102 "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
5.103 by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus
5.104 - hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric]
5.105 add_ac mult_ac right_distrib)
5.106
5.107 (*HComplex_inverse is proved below*)
5.108 @@ -1000,7 +996,9 @@
5.109 hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
5.110 iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
5.111 apply (cases x, cases y)
5.112 -apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
5.113 +apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def
5.114 + starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide
5.115 + hcomplex_diff numeral_2_eq_2 complex_of_real_def i_def)
5.116 apply (simp add: diff_minus)
5.117 done
5.118
5.119 @@ -1163,8 +1161,7 @@
5.120 "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
5.121 apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
5.122 apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
5.123 - hcomplex_mult cis_mult [symmetric]
5.124 - complex_of_real_mult [symmetric])
5.125 + hcomplex_mult cis_mult [symmetric])
5.126 done
5.127
5.128 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
5.129 @@ -1304,17 +1301,28 @@
5.130
5.131 lemma hcomplex_of_complex_inverse [simp]:
5.132 "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
5.133 -apply (case_tac "r=0")
5.134 -apply (simp add: hcomplex_of_complex_zero)
5.135 -apply (rule_tac c1 = "hcomplex_of_complex r"
5.136 - in hcomplex_mult_left_cancel [THEN iffD1])
5.137 -apply (force simp add: hcomplex_of_complex_zero_iff)
5.138 -apply (subst hcomplex_of_complex_mult [symmetric])
5.139 -apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
5.140 -done
5.141 +proof cases
5.142 + assume "r=0" thus ?thesis by simp
5.143 +next
5.144 + assume nz: "r\<noteq>0"
5.145 + show ?thesis
5.146 + proof (rule hcomplex_mult_left_cancel [THEN iffD1])
5.147 + show "hcomplex_of_complex r \<noteq> 0"
5.148 + by (simp add: nz)
5.149 + next
5.150 + have "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
5.151 + hcomplex_of_complex (r * inverse r)"
5.152 + by simp
5.153 + also have "... = hcomplex_of_complex r * inverse (hcomplex_of_complex r)"
5.154 + by (simp add: nz)
5.155 + finally show "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
5.156 + hcomplex_of_complex r * inverse (hcomplex_of_complex r)" .
5.157 + qed
5.158 +qed
5.159
5.160 lemma hcomplex_of_complex_divide [simp]:
5.161 - "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
5.162 + "hcomplex_of_complex (z1 / z2) =
5.163 + hcomplex_of_complex z1 / hcomplex_of_complex z2"
5.164 by (simp add: hcomplex_divide_def complex_divide_def)
5.165
5.166 lemma hRe_hcomplex_of_complex:
5.167 @@ -1334,38 +1342,38 @@
5.168
5.169 instance hcomplex :: number ..
5.170
5.171 -primrec (*the type constraint is essential!*)
5.172 - number_of_Pls: "number_of bin.Pls = 0"
5.173 - number_of_Min: "number_of bin.Min = - (1::hcomplex)"
5.174 - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
5.175 - (number_of w) + (number_of w)"
5.176 -
5.177 -declare number_of_Pls [simp del]
5.178 - number_of_Min [simp del]
5.179 - number_of_BIT [simp del]
5.180 +defs (overloaded)
5.181 + hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
5.182 + --{*the type constraint is essential!*}
5.183
5.184 instance hcomplex :: number_ring
5.185 -proof
5.186 - show "Numeral0 = (0::hcomplex)" by (rule number_of_Pls)
5.187 - show "-1 = - (1::hcomplex)" by (rule number_of_Min)
5.188 - fix w :: bin and x :: bool
5.189 - show "(number_of (w BIT x) :: hcomplex) =
5.190 - (if x then 1 else 0) + number_of w + number_of w"
5.191 - by (rule number_of_BIT)
5.192 +by (intro_classes, simp add: hcomplex_number_of_def)
5.193 +
5.194 +
5.195 +lemma hcomplex_of_complex_of_nat [simp]:
5.196 + "hcomplex_of_complex (of_nat n) = of_nat n"
5.197 +by (induct n, simp_all)
5.198 +
5.199 +lemma hcomplex_of_complex_of_int [simp]:
5.200 + "hcomplex_of_complex (of_int z) = of_int z"
5.201 +proof (cases z)
5.202 + case (1 n)
5.203 + thus ?thesis by simp
5.204 +next
5.205 + case (2 n)
5.206 + thus ?thesis
5.207 + by (simp only: of_int_minus hcomplex_of_complex_minus, simp)
5.208 qed
5.209
5.210
5.211 text{*Collapse applications of @{term hcomplex_of_complex} to @{term number_of}*}
5.212 lemma hcomplex_number_of [simp]:
5.213 "hcomplex_of_complex (number_of w) = number_of w"
5.214 -apply (induct w)
5.215 -apply (simp_all only: number_of hcomplex_of_complex_add
5.216 - hcomplex_of_complex_minus, simp_all)
5.217 -done
5.218 +by (simp add: hcomplex_number_of_def complex_number_of_def)
5.219
5.220 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
5.221 "hcomplex_of_hypreal (hypreal_of_real x) =
5.222 - hcomplex_of_complex(complex_of_real x)"
5.223 + hcomplex_of_complex (complex_of_real x)"
5.224 by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def
5.225 complex_of_real_def)
5.226
6.1 --- a/src/HOL/Hyperreal/HTranscendental.thy Wed Jun 30 14:04:58 2004 +0200
6.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy Thu Jul 01 12:29:53 2004 +0200
6.3 @@ -9,6 +9,25 @@
6.4
6.5 theory HTranscendental = Transcendental + Integration:
6.6
6.7 +text{*really belongs in Transcendental*}
6.8 +lemma sqrt_divide_self_eq:
6.9 + assumes nneg: "0 \<le> x"
6.10 + shows "sqrt x / x = inverse (sqrt x)"
6.11 +proof cases
6.12 + assume "x=0" thus ?thesis by simp
6.13 +next
6.14 + assume nz: "x\<noteq>0"
6.15 + hence pos: "0<x" using nneg by arith
6.16 + show ?thesis
6.17 + proof (rule right_inverse_eq [THEN iffD1, THEN sym])
6.18 + show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz)
6.19 + show "inverse (sqrt x) / (sqrt x / x) = 1"
6.20 + by (simp add: divide_inverse mult_assoc [symmetric]
6.21 + power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz)
6.22 + qed
6.23 +qed
6.24 +
6.25 +
6.26 constdefs
6.27
6.28 exphr :: "real => hypreal"
7.1 --- a/src/HOL/Hyperreal/HyperArith.thy Wed Jun 30 14:04:58 2004 +0200
7.2 +++ b/src/HOL/Hyperreal/HyperArith.thy Thu Jul 01 12:29:53 2004 +0200
7.3 @@ -14,32 +14,18 @@
7.4
7.5 instance hypreal :: number ..
7.6
7.7 -primrec (*the type constraint is essential!*)
7.8 - number_of_Pls: "number_of bin.Pls = 0"
7.9 - number_of_Min: "number_of bin.Min = - (1::hypreal)"
7.10 - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
7.11 - (number_of w) + (number_of w)"
7.12 -
7.13 -declare number_of_Pls [simp del]
7.14 - number_of_Min [simp del]
7.15 - number_of_BIT [simp del]
7.16 +defs (overloaded)
7.17 + hypreal_number_of_def: "(number_of w :: hypreal) == of_int (Rep_Bin w)"
7.18 + --{*the type constraint is essential!*}
7.19
7.20 instance hypreal :: number_ring
7.21 -proof
7.22 - show "Numeral0 = (0::hypreal)" by (rule number_of_Pls)
7.23 - show "-1 = - (1::hypreal)" by (rule number_of_Min)
7.24 - fix w :: bin and x :: bool
7.25 - show "(number_of (w BIT x) :: hypreal) =
7.26 - (if x then 1 else 0) + number_of w + number_of w"
7.27 - by (rule number_of_BIT)
7.28 -qed
7.29 +by (intro_classes, simp add: hypreal_number_of_def)
7.30
7.31
7.32 text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*}
7.33 lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
7.34 -apply (induct w)
7.35 -apply (simp_all only: number_of hypreal_of_real_add hypreal_of_real_minus, simp_all)
7.36 -done
7.37 +by (simp add: hypreal_number_of_def real_number_of_def)
7.38 +
7.39
7.40
7.41 use "hypreal_arith.ML"
8.1 --- a/src/HOL/Hyperreal/HyperDef.thy Wed Jun 30 14:04:58 2004 +0200
8.2 +++ b/src/HOL/Hyperreal/HyperDef.thy Thu Jul 01 12:29:53 2004 +0200
8.3 @@ -526,6 +526,14 @@
8.4 "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
8.5 by (simp add: hypreal_of_real_def, simp add: hypreal_add left_distrib)
8.6
8.7 +lemma hypreal_of_real_minus [simp]:
8.8 + "hypreal_of_real (-r) = - hypreal_of_real r"
8.9 +by (auto simp add: hypreal_of_real_def hypreal_minus)
8.10 +
8.11 +lemma hypreal_of_real_diff [simp]:
8.12 + "hypreal_of_real (w - z) = hypreal_of_real w - hypreal_of_real z"
8.13 +by (simp add: diff_minus)
8.14 +
8.15 lemma hypreal_of_real_mult [simp]:
8.16 "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
8.17 by (simp add: hypreal_of_real_def, simp add: hypreal_mult right_distrib)
8.18 @@ -572,10 +580,6 @@
8.19 declare hypreal_of_real_le_iff [of _ 1, simplified, simp]
8.20 declare hypreal_of_real_eq_iff [of _ 1, simplified, simp]
8.21
8.22 -lemma hypreal_of_real_minus [simp]:
8.23 - "hypreal_of_real (-r) = - hypreal_of_real r"
8.24 -by (auto simp add: hypreal_of_real_def hypreal_minus)
8.25 -
8.26 lemma hypreal_of_real_inverse [simp]:
8.27 "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
8.28 apply (case_tac "r=0", simp)
8.29 @@ -587,6 +591,19 @@
8.30 "hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z"
8.31 by (simp add: hypreal_divide_def real_divide_def)
8.32
8.33 +lemma hypreal_of_real_of_nat [simp]: "hypreal_of_real (of_nat n) = of_nat n"
8.34 +by (induct n, simp_all)
8.35 +
8.36 +lemma hypreal_of_real_of_int [simp]: "hypreal_of_real (of_int z) = of_int z"
8.37 +proof (cases z)
8.38 + case (1 n)
8.39 + thus ?thesis by simp
8.40 +next
8.41 + case (2 n)
8.42 + thus ?thesis
8.43 + by (simp only: of_int_minus hypreal_of_real_minus, simp)
8.44 +qed
8.45 +
8.46
8.47 subsection{*Misc Others*}
8.48
9.1 --- a/src/HOL/Hyperreal/Transcendental.thy Wed Jun 30 14:04:58 2004 +0200
9.2 +++ b/src/HOL/Hyperreal/Transcendental.thy Thu Jul 01 12:29:53 2004 +0200
9.3 @@ -8,42 +8,42 @@
9.4 Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim +
9.5
9.6 constdefs
9.7 - root :: [nat,real] => real
9.8 + root :: "[nat,real] => real"
9.9 "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
9.10
9.11 - sqrt :: real => real
9.12 + sqrt :: "real => real"
9.13 "sqrt x == root 2 x"
9.14
9.15 - exp :: real => real
9.16 + exp :: "real => real"
9.17 "exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"
9.18
9.19 - sin :: real => real
9.20 + sin :: "real => real"
9.21 "sin x == suminf(%n. (if even(n) then 0 else
9.22 ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
9.23
9.24 - diffs :: (nat => real) => nat => real
9.25 + diffs :: "(nat => real) => nat => real"
9.26 "diffs c == (%n. real (Suc n) * c(Suc n))"
9.27
9.28 - cos :: real => real
9.29 + cos :: "real => real"
9.30 "cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n))
9.31 else 0) * x ^ n)"
9.32
9.33 - ln :: real => real
9.34 + ln :: "real => real"
9.35 "ln x == (@u. exp u = x)"
9.36
9.37 - pi :: real
9.38 + pi :: "real"
9.39 "pi == 2 * (@x. 0 <= (x::real) & x <= 2 & cos x = 0)"
9.40
9.41 - tan :: real => real
9.42 + tan :: "real => real"
9.43 "tan x == (sin x)/(cos x)"
9.44
9.45 - arcsin :: real => real
9.46 + arcsin :: "real => real"
9.47 "arcsin y == (@x. -(pi/2) <= x & x <= pi/2 & sin x = y)"
9.48
9.49 - arcos :: real => real
9.50 + arcos :: "real => real"
9.51 "arcos y == (@x. 0 <= x & x <= pi & cos x = y)"
9.52
9.53 - arctan :: real => real
9.54 + arctan :: "real => real"
9.55 "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
9.56
9.57 end
10.1 --- a/src/HOL/Import/HOL/HOL4Prob.thy Wed Jun 30 14:04:58 2004 +0200
10.2 +++ b/src/HOL/Import/HOL/HOL4Prob.thy Thu Jul 01 12:29:53 2004 +0200
10.3 @@ -27,7 +27,7 @@
10.4 ((op *::nat => nat => nat)
10.5 ((number_of::bin => nat)
10.6 ((op BIT::bin => bool => bin)
10.7 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.8 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.9 (True::bool))
10.10 (False::bool)))
10.11 q)
10.12 @@ -40,14 +40,14 @@
10.13 ((op div::nat => nat => nat) n
10.14 ((number_of::bin => nat)
10.15 ((op BIT::bin => bool => bin)
10.16 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.17 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.18 (True::bool))
10.19 (False::bool)))))
10.20 ((op =::nat => nat => bool) r
10.21 ((op mod::nat => nat => nat) n
10.22 ((number_of::bin => nat)
10.23 ((op BIT::bin => bool => bin)
10.24 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.25 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.26 (True::bool))
10.27 (False::bool)))))))))"
10.28 by (import prob_extra DIV_TWO_UNIQUE)
10.29 @@ -76,13 +76,13 @@
10.30 ((op div::nat => nat => nat) m
10.31 ((number_of::bin => nat)
10.32 ((op BIT::bin => bool => bin)
10.33 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.34 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.35 (True::bool))
10.36 (False::bool))))
10.37 ((op div::nat => nat => nat) n
10.38 ((number_of::bin => nat)
10.39 ((op BIT::bin => bool => bin)
10.40 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.41 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.42 (True::bool))
10.43 (False::bool)))))
10.44 ((op <::nat => nat => bool) m n)))"
10.45 @@ -98,13 +98,13 @@
10.46 ((op div::nat => nat => nat) m
10.47 ((number_of::bin => nat)
10.48 ((op BIT::bin => bool => bin)
10.49 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.50 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.51 (True::bool))
10.52 (False::bool))))
10.53 ((op div::nat => nat => nat) n
10.54 ((number_of::bin => nat)
10.55 ((op BIT::bin => bool => bin)
10.56 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.57 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.58 (True::bool))
10.59 (False::bool)))))
10.60 ((op <::nat => nat => bool) m n))))"
10.61 @@ -204,7 +204,7 @@
10.62 ((op /::real => real => real) (1::real)
10.63 ((number_of::bin => real)
10.64 ((op BIT::bin => bool => bin)
10.65 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.66 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.67 (True::bool))
10.68 (False::bool))))
10.69 n)
10.70 @@ -212,7 +212,7 @@
10.71 ((op /::real => real => real) (1::real)
10.72 ((number_of::bin => real)
10.73 ((op BIT::bin => bool => bin)
10.74 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.75 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.76 (True::bool))
10.77 (False::bool))))
10.78 m))))"
10.79 @@ -2528,7 +2528,7 @@
10.80 ((op /::real => real => real) (1::real)
10.81 ((number_of::bin => real)
10.82 ((op BIT::bin => bool => bin)
10.83 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.84 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.85 (True::bool))
10.86 (False::bool))))
10.87 ((prob::((nat => bool) => bool) => real) p)))))"
10.88 @@ -3156,7 +3156,7 @@
10.89 ((op /::real => real => real) (1::real)
10.90 ((number_of::bin => real)
10.91 ((op BIT::bin => bool => bin)
10.92 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.93 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.94 (True::bool))
10.95 (False::bool))))
10.96 ((size::bool list => nat) x))
10.97 @@ -3382,7 +3382,7 @@
10.98 (P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
10.99 ((number_of::bin => nat)
10.100 ((op BIT::bin => bool => bin)
10.101 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.102 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.103 (True::bool))
10.104 (False::bool)))))
10.105 (P ((Suc::nat => nat) v)))))
10.106 @@ -3436,7 +3436,7 @@
10.107 (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
10.108 ((number_of::bin => nat)
10.109 ((op BIT::bin => bool => bin)
10.110 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.111 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.112 (True::bool))
10.113 (False::bool))))
10.114 s)
10.115 @@ -3716,13 +3716,13 @@
10.116 ((op ^::nat => nat => nat)
10.117 ((number_of::bin => nat)
10.118 ((op BIT::bin => bool => bin)
10.119 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
10.120 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
10.121 (False::bool)))
10.122 ((unif_bound::nat => nat) n))
10.123 ((op *::nat => nat => nat)
10.124 ((number_of::bin => nat)
10.125 ((op BIT::bin => bool => bin)
10.126 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
10.127 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
10.128 (False::bool)))
10.129 n)))"
10.130 by (import prob_uniform UNIF_BOUND_UPPER)
10.131 @@ -3771,7 +3771,7 @@
10.132 ((op ^::nat => nat => nat)
10.133 ((number_of::bin => nat)
10.134 ((op BIT::bin => bool => bin)
10.135 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.136 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.137 (True::bool))
10.138 (False::bool)))
10.139 ((unif_bound::nat => nat) n)))
10.140 @@ -3788,7 +3788,7 @@
10.141 ((op /::real => real => real) (1::real)
10.142 ((number_of::bin => real)
10.143 ((op BIT::bin => bool => bin)
10.144 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.145 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.146 (True::bool))
10.147 (False::bool))))
10.148 ((unif_bound::nat => nat) n))))))"
10.149 @@ -3907,7 +3907,7 @@
10.150 ((op /::real => real => real) (1::real)
10.151 ((number_of::bin => real)
10.152 ((op BIT::bin => bool => bin)
10.153 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.154 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.155 (True::bool))
10.156 (False::bool))))
10.157 t))))))"
10.158 @@ -3938,7 +3938,7 @@
10.159 ((op /::real => real => real) (1::real)
10.160 ((number_of::bin => real)
10.161 ((op BIT::bin => bool => bin)
10.162 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.163 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.164 (True::bool))
10.165 (False::bool))))
10.166 t)))))"
10.167 @@ -3969,7 +3969,7 @@
10.168 ((op /::real => real => real) (1::real)
10.169 ((number_of::bin => real)
10.170 ((op BIT::bin => bool => bin)
10.171 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
10.172 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
10.173 (True::bool))
10.174 (False::bool))))
10.175 t)))))"
11.1 --- a/src/HOL/Import/HOL/HOL4Real.thy Wed Jun 30 14:04:58 2004 +0200
11.2 +++ b/src/HOL/Import/HOL/HOL4Real.thy Thu Jul 01 12:29:53 2004 +0200
11.3 @@ -1916,13 +1916,13 @@
11.4 ((op *::nat => nat => nat)
11.5 ((number_of::bin => nat)
11.6 ((op BIT::bin => bool => bin)
11.7 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.8 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.9 (True::bool))
11.10 (False::bool)))
11.11 n)
11.12 ((number_of::bin => nat)
11.13 ((op BIT::bin => bool => bin)
11.14 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.15 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.16 (True::bool))
11.17 (False::bool))))
11.18 f)
11.19 @@ -1958,7 +1958,7 @@
11.20 ((number_of::bin => nat)
11.21 ((op BIT::bin => bool => bin)
11.22 ((op BIT::bin => bool => bin)
11.23 - (bin.Pls::bin) (True::bool))
11.24 + (Numeral.Pls::bin) (True::bool))
11.25 (False::bool)))
11.26 d)))
11.27 (f ((op +::nat => nat => nat) n
11.28 @@ -1967,7 +1967,7 @@
11.29 ((number_of::bin => nat)
11.30 ((op BIT::bin => bool => bin)
11.31 ((op BIT::bin => bool => bin)
11.32 - (bin.Pls::bin) (True::bool))
11.33 + (Numeral.Pls::bin) (True::bool))
11.34 (False::bool)))
11.35 d)
11.36 (1::nat))))))))
11.37 @@ -2825,7 +2825,7 @@
11.38 ((op ^::real => nat => real) ((inverse::real => real) x)
11.39 ((number_of::bin => nat)
11.40 ((op BIT::bin => bool => bin)
11.41 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.42 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.43 (False::bool)))))
11.44 x))"
11.45 by (import lim DIFF_XM1)
11.46 @@ -2848,7 +2848,7 @@
11.47 ((op ^::real => nat => real) (f x)
11.48 ((number_of::bin => nat)
11.49 ((op BIT::bin => bool => bin)
11.50 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.51 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.52 (True::bool))
11.53 (False::bool))))))
11.54 x))))"
11.55 @@ -2886,7 +2886,7 @@
11.56 ((number_of::bin => nat)
11.57 ((op BIT::bin => bool => bin)
11.58 ((op BIT::bin => bool => bin)
11.59 -(bin.Pls::bin) (True::bool))
11.60 +(Numeral.Pls::bin) (True::bool))
11.61 (False::bool)))))
11.62 x))))))"
11.63 by (import lim DIFF_DIV)
11.64 @@ -3869,7 +3869,7 @@
11.65 ((op -::nat => nat => nat) n
11.66 ((number_of::bin => nat)
11.67 ((op BIT::bin => bool => bin)
11.68 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.69 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.70 (False::bool))))
11.71 p)
11.72 q)))))))))))"
11.73 @@ -3917,7 +3917,7 @@
11.74 ((number_of::bin => nat)
11.75 ((op BIT::bin => bool => bin)
11.76 ((op BIT::bin => bool => bin)
11.77 - (bin.Pls::bin) (True::bool))
11.78 + (Numeral.Pls::bin) (True::bool))
11.79 (False::bool)))))
11.80 ((abs::real => real) h)))))))))"
11.81 by (import powser TERMDIFF_LEMMA3)
11.82 @@ -4112,7 +4112,7 @@
11.83 ((op ^::real => nat => real) (f x)
11.84 ((number_of::bin => nat)
11.85 ((op BIT::bin => bool => bin)
11.86 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.87 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.88 (False::bool))))))
11.89 x))
11.90 ((op &::bool => bool => bool)
11.91 @@ -4133,7 +4133,7 @@
11.92 ((op ^::real => nat => real) (g x)
11.93 ((number_of::bin => nat)
11.94 ((op BIT::bin => bool => bin)
11.95 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.96 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.97 (False::bool)))))
11.98 x))
11.99 ((op &::bool => bool => bool)
11.100 @@ -4652,7 +4652,7 @@
11.101 ((op ^::real => nat => real) ((sqrt::real => real) x)
11.102 ((number_of::bin => nat)
11.103 ((op BIT::bin => bool => bin)
11.104 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.105 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.106 (False::bool))))
11.107 x))"
11.108 by (import transc SQRT_POW_2)
11.109 @@ -4664,7 +4664,7 @@
11.110 ((op ^::real => nat => real) x
11.111 ((number_of::bin => nat)
11.112 ((op BIT::bin => bool => bin)
11.113 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.114 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.115 (False::bool)))))
11.116 x)"
11.117 by (import transc POW_2_SQRT)
11.118 @@ -4682,7 +4682,7 @@
11.119 ((op ^::real => nat => real) xa
11.120 ((number_of::bin => nat)
11.121 ((op BIT::bin => bool => bin)
11.122 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.123 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.124 (True::bool))
11.125 (False::bool))))
11.126 x)))
11.127 @@ -4746,18 +4746,18 @@
11.128 ((op ^::real => nat => real)
11.129 ((number_of::bin => real)
11.130 ((op BIT::bin => bool => bin)
11.131 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.132 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.133 (False::bool)))
11.134 n))
11.135 ((op ^::real => nat => real)
11.136 ((number_of::bin => real)
11.137 ((op BIT::bin => bool => bin)
11.138 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.139 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.140 (False::bool)))
11.141 ((op div::nat => nat => nat) n
11.142 ((number_of::bin => nat)
11.143 ((op BIT::bin => bool => bin)
11.144 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.145 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.146 (False::bool)))))))"
11.147 by (import transc SQRT_EVEN_POW2)
11.148
11.149 @@ -4780,7 +4780,7 @@
11.150 ((op ^::real => nat => real) x
11.151 ((number_of::bin => nat)
11.152 ((op BIT::bin => bool => bin)
11.153 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.154 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.155 (True::bool))
11.156 (False::bool))))
11.157 y)
11.158 @@ -4848,7 +4848,7 @@
11.159 ((op <::real => real => bool) x
11.160 ((number_of::bin => real)
11.161 ((op BIT::bin => bool => bin)
11.162 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.163 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.164 (False::bool)))))
11.165 ((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
11.166 by (import transc SIN_POS)
11.167 @@ -4923,7 +4923,7 @@
11.168 ((op /::real => real => real) (pi::real)
11.169 ((number_of::bin => real)
11.170 ((op BIT::bin => bool => bin)
11.171 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.172 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.173 (False::bool))))))
11.174 ((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
11.175 by (import transc SIN_POS_PI2)
11.176 @@ -4937,7 +4937,7 @@
11.177 ((op /::real => real => real) (pi::real)
11.178 ((number_of::bin => real)
11.179 ((op BIT::bin => bool => bin)
11.180 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.181 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.182 (False::bool))))))
11.183 ((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
11.184 by (import transc COS_POS_PI2)
11.185 @@ -4951,14 +4951,14 @@
11.186 ((op /::real => real => real) (pi::real)
11.187 ((number_of::bin => real)
11.188 ((op BIT::bin => bool => bin)
11.189 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.190 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.191 (False::bool)))))
11.192 x)
11.193 ((op <::real => real => bool) x
11.194 ((op /::real => real => real) (pi::real)
11.195 ((number_of::bin => real)
11.196 ((op BIT::bin => bool => bin)
11.197 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.198 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.199 (False::bool))))))
11.200 ((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
11.201 by (import transc COS_POS_PI)
11.202 @@ -4981,7 +4981,7 @@
11.203 ((op /::real => real => real) (pi::real)
11.204 ((number_of::bin => real)
11.205 ((op BIT::bin => bool => bin)
11.206 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.207 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.208 (False::bool))))))
11.209 ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
11.210 by (import transc COS_POS_PI2_LE)
11.211 @@ -4995,14 +4995,14 @@
11.212 ((op /::real => real => real) (pi::real)
11.213 ((number_of::bin => real)
11.214 ((op BIT::bin => bool => bin)
11.215 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.216 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.217 (False::bool)))))
11.218 x)
11.219 ((op <=::real => real => bool) x
11.220 ((op /::real => real => real) (pi::real)
11.221 ((number_of::bin => real)
11.222 ((op BIT::bin => bool => bin)
11.223 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.224 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.225 (False::bool))))))
11.226 ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
11.227 by (import transc COS_POS_PI_LE)
11.228 @@ -5016,7 +5016,7 @@
11.229 ((op /::real => real => real) (pi::real)
11.230 ((number_of::bin => real)
11.231 ((op BIT::bin => bool => bin)
11.232 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.233 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.234 (False::bool))))))
11.235 ((op <=::real => real => bool) (0::real) ((sin::real => real) x)))"
11.236 by (import transc SIN_POS_PI2_LE)
11.237 @@ -5059,7 +5059,7 @@
11.238 ((op /::real => real => real) (pi::real)
11.239 ((number_of::bin => real)
11.240 ((op BIT::bin => bool => bin)
11.241 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.242 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.243 (True::bool))
11.244 (False::bool)))))
11.245 x)
11.246 @@ -5068,7 +5068,7 @@
11.247 ((op /::real => real => real) (pi::real)
11.248 ((number_of::bin => real)
11.249 ((op BIT::bin => bool => bin)
11.250 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.251 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.252 (True::bool))
11.253 (False::bool)))))
11.254 ((op =::real => real => bool) ((sin::real => real) x) y)))))"
11.255 @@ -5089,7 +5089,7 @@
11.256 ((op /::real => real => real) (pi::real)
11.257 ((number_of::bin => real)
11.258 ((op BIT::bin => bool => bin)
11.259 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.260 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.261 (True::bool))
11.262 (False::bool)))))))))"
11.263 by (import transc COS_ZERO_LEMMA)
11.264 @@ -5108,7 +5108,7 @@
11.265 ((op /::real => real => real) (pi::real)
11.266 ((number_of::bin => real)
11.267 ((op BIT::bin => bool => bin)
11.268 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.269 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.270 (True::bool))
11.271 (False::bool)))))))))"
11.272 by (import transc SIN_ZERO_LEMMA)
11.273 @@ -5186,7 +5186,7 @@
11.274 ((op *::real => real => real)
11.275 ((number_of::bin => real)
11.276 ((op BIT::bin => bool => bin)
11.277 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.278 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.279 (True::bool))
11.280 (False::bool)))
11.281 x))
11.282 @@ -5196,21 +5196,21 @@
11.283 ((op *::real => real => real)
11.284 ((number_of::bin => real)
11.285 ((op BIT::bin => bool => bin)
11.286 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.287 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.288 (False::bool)))
11.289 x))
11.290 ((op /::real => real => real)
11.291 ((op *::real => real => real)
11.292 ((number_of::bin => real)
11.293 ((op BIT::bin => bool => bin)
11.294 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.295 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.296 (False::bool)))
11.297 ((tan::real => real) x))
11.298 ((op -::real => real => real) (1::real)
11.299 ((op ^::real => nat => real) ((tan::real => real) x)
11.300 ((number_of::bin => nat)
11.301 ((op BIT::bin => bool => bin)
11.302 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.303 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.304 (False::bool))))))))"
11.305 by (import transc TAN_DOUBLE)
11.306
11.307 @@ -5223,7 +5223,7 @@
11.308 ((op /::real => real => real) (pi::real)
11.309 ((number_of::bin => real)
11.310 ((op BIT::bin => bool => bin)
11.311 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.312 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.313 (False::bool))))))
11.314 ((op <::real => real => bool) (0::real) ((tan::real => real) x)))"
11.315 by (import transc TAN_POS_PI2)
11.316 @@ -5238,7 +5238,7 @@
11.317 ((op ^::real => nat => real) ((cos::real => real) x)
11.318 ((number_of::bin => nat)
11.319 ((op BIT::bin => bool => bin)
11.320 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.321 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.322 (False::bool)))))
11.323 x))"
11.324 by (import transc DIFF_TAN)
11.325 @@ -5256,7 +5256,7 @@
11.326 ((op /::real => real => real) (pi::real)
11.327 ((number_of::bin => real)
11.328 ((op BIT::bin => bool => bin)
11.329 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.330 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.331 (True::bool))
11.332 (False::bool)))))
11.333 ((op <::real => real => bool) y ((tan::real => real) x))))))"
11.334 @@ -5275,7 +5275,7 @@
11.335 ((op /::real => real => real) (pi::real)
11.336 ((number_of::bin => real)
11.337 ((op BIT::bin => bool => bin)
11.338 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.339 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.340 (True::bool))
11.341 (False::bool)))))
11.342 ((op =::real => real => bool) ((tan::real => real) x) y)))))"
11.343 @@ -5317,7 +5317,7 @@
11.344 ((op /::real => real => real) (pi::real)
11.345 ((number_of::bin => real)
11.346 ((op BIT::bin => bool => bin)
11.347 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.348 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.349 (False::bool)))))
11.350 ((asn::real => real) y))
11.351 ((op &::bool => bool => bool)
11.352 @@ -5325,7 +5325,7 @@
11.353 ((op /::real => real => real) (pi::real)
11.354 ((number_of::bin => real)
11.355 ((op BIT::bin => bool => bin)
11.356 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.357 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.358 (False::bool)))))
11.359 ((op =::real => real => bool)
11.360 ((sin::real => real) ((asn::real => real) y)) y))))"
11.361 @@ -5353,14 +5353,14 @@
11.362 ((op /::real => real => real) (pi::real)
11.363 ((number_of::bin => real)
11.364 ((op BIT::bin => bool => bin)
11.365 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.366 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.367 (False::bool)))))
11.368 ((asn::real => real) y))
11.369 ((op <=::real => real => bool) ((asn::real => real) y)
11.370 ((op /::real => real => real) (pi::real)
11.371 ((number_of::bin => real)
11.372 ((op BIT::bin => bool => bin)
11.373 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.374 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.375 (False::bool)))))))"
11.376 by (import transc ASN_BOUNDS)
11.377
11.378 @@ -5376,14 +5376,14 @@
11.379 ((op /::real => real => real) (pi::real)
11.380 ((number_of::bin => real)
11.381 ((op BIT::bin => bool => bin)
11.382 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.383 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.384 (False::bool)))))
11.385 ((asn::real => real) y))
11.386 ((op <::real => real => bool) ((asn::real => real) y)
11.387 ((op /::real => real => real) (pi::real)
11.388 ((number_of::bin => real)
11.389 ((op BIT::bin => bool => bin)
11.390 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.391 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.392 (False::bool)))))))"
11.393 by (import transc ASN_BOUNDS_LT)
11.394
11.395 @@ -5396,14 +5396,14 @@
11.396 ((op /::real => real => real) (pi::real)
11.397 ((number_of::bin => real)
11.398 ((op BIT::bin => bool => bin)
11.399 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.400 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.401 (False::bool)))))
11.402 x)
11.403 ((op <=::real => real => bool) x
11.404 ((op /::real => real => real) (pi::real)
11.405 ((number_of::bin => real)
11.406 ((op BIT::bin => bool => bin)
11.407 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.408 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.409 (False::bool))))))
11.410 ((op =::real => real => bool)
11.411 ((asn::real => real) ((sin::real => real) x)) x))"
11.412 @@ -5483,14 +5483,14 @@
11.413 ((op /::real => real => real) (pi::real)
11.414 ((number_of::bin => real)
11.415 ((op BIT::bin => bool => bin)
11.416 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.417 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.418 (False::bool)))))
11.419 x)
11.420 ((op <::real => real => bool) x
11.421 ((op /::real => real => real) (pi::real)
11.422 ((number_of::bin => real)
11.423 ((op BIT::bin => bool => bin)
11.424 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.425 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.426 (False::bool))))))
11.427 ((op =::real => real => bool)
11.428 ((atn::real => real) ((tan::real => real) x)) x))"
11.429 @@ -5506,13 +5506,13 @@
11.430 ((op ^::real => nat => real) ((tan::real => real) x)
11.431 ((number_of::bin => nat)
11.432 ((op BIT::bin => bool => bin)
11.433 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.434 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.435 (False::bool)))))
11.436 ((op ^::real => nat => real)
11.437 ((inverse::real => real) ((cos::real => real) x))
11.438 ((number_of::bin => nat)
11.439 ((op BIT::bin => bool => bin)
11.440 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.441 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.442 (False::bool))))))"
11.443 by (import transc TAN_SEC)
11.444
11.445 @@ -5528,7 +5528,7 @@
11.446 ((op ^::real => nat => real) ((cos::real => real) x)
11.447 ((number_of::bin => nat)
11.448 ((op BIT::bin => bool => bin)
11.449 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.450 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.451 (False::bool))))))))"
11.452 by (import transc SIN_COS_SQ)
11.453
11.454 @@ -5541,14 +5541,14 @@
11.455 ((op /::real => real => real) (pi::real)
11.456 ((number_of::bin => real)
11.457 ((op BIT::bin => bool => bin)
11.458 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.459 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.460 (False::bool)))))
11.461 x)
11.462 ((op <=::real => real => bool) x
11.463 ((op /::real => real => real) (pi::real)
11.464 ((number_of::bin => real)
11.465 ((op BIT::bin => bool => bin)
11.466 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.467 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.468 (False::bool))))))
11.469 ((op =::real => real => bool) ((cos::real => real) x)
11.470 ((sqrt::real => real)
11.471 @@ -5556,7 +5556,7 @@
11.472 ((op ^::real => nat => real) ((sin::real => real) x)
11.473 ((number_of::bin => nat)
11.474 ((op BIT::bin => bool => bin)
11.475 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.476 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.477 (False::bool))))))))"
11.478 by (import transc COS_SIN_SQ)
11.479
11.480 @@ -5595,7 +5595,7 @@
11.481 ((op ^::real => nat => real) ((sin::real => real) x)
11.482 ((number_of::bin => nat)
11.483 ((op BIT::bin => bool => bin)
11.484 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.485 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.486 (False::bool))))))))"
11.487 by (import transc COS_SIN_SQRT)
11.488
11.489 @@ -5609,7 +5609,7 @@
11.490 ((op ^::real => nat => real) ((cos::real => real) x)
11.491 ((number_of::bin => nat)
11.492 ((op BIT::bin => bool => bin)
11.493 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
11.494 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
11.495 (False::bool))))))))"
11.496 by (import transc SIN_COS_SQRT)
11.497
11.498 @@ -5646,7 +5646,7 @@
11.499 ((op ^::real => nat => real) x
11.500 ((number_of::bin => nat)
11.501 ((op BIT::bin => bool => bin)
11.502 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.503 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.504 (True::bool))
11.505 (False::bool)))))))
11.506 x))"
11.507 @@ -5679,7 +5679,7 @@
11.508 ((op ^::real => nat => real) x
11.509 ((number_of::bin => nat)
11.510 ((op BIT::bin => bool => bin)
11.511 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
11.512 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
11.513 (True::bool))
11.514 (False::bool))))))))
11.515 x))"
12.1 --- a/src/HOL/Import/HOL/HOL4Vec.thy Wed Jun 30 14:04:58 2004 +0200
12.2 +++ b/src/HOL/Import/HOL/HOL4Vec.thy Thu Jul 01 12:29:53 2004 +0200
12.3 @@ -1103,7 +1103,7 @@
12.4 ((op <::nat => nat => bool) x
12.5 ((number_of::bin => nat)
12.6 ((op BIT::bin => bool => bin)
12.7 - ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
12.8 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
12.9 (False::bool))))
12.10 ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
12.11 x))"
12.12 @@ -1298,7 +1298,7 @@
12.13 ((op ^::nat => nat => nat)
12.14 ((number_of::bin => nat)
12.15 ((op BIT::bin => bool => bin)
12.16 - ((op BIT::bin => bool => bin) (bin.Pls::bin)
12.17 + ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
12.18 (True::bool))
12.19 (False::bool)))
12.20 k)))))))"
13.1 --- a/src/HOL/Integ/Bin.thy Wed Jun 30 14:04:58 2004 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,351 +0,0 @@
13.4 -(* Title: HOL/Integ/Bin.thy
13.5 - ID: $Id$
13.6 - Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
13.7 - Copyright 1994 University of Cambridge
13.8 -
13.9 -Ported from ZF to HOL by David Spelt.
13.10 -*)
13.11 -
13.12 -header{*Arithmetic on Binary Integers*}
13.13 -
13.14 -theory Bin = IntDef + Numeral:
13.15 -
13.16 -axclass number_ring \<subseteq> number, comm_ring_1
13.17 - number_of_Pls: "number_of bin.Pls = 0"
13.18 - number_of_Min: "number_of bin.Min = - 1"
13.19 - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
13.20 - (number_of w) + (number_of w)"
13.21 -subsection{*Converting Numerals to Rings: @{term number_of}*}
13.22 -
13.23 -lemmas number_of = number_of_Pls number_of_Min number_of_BIT
13.24 -
13.25 -lemma number_of_NCons [simp]:
13.26 - "number_of(NCons w b) = (number_of(w BIT b)::'a::number_ring)"
13.27 -by (induct_tac "w", simp_all add: number_of)
13.28 -
13.29 -lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
13.30 -apply (induct_tac "w")
13.31 -apply (simp_all add: number_of add_ac)
13.32 -done
13.33 -
13.34 -lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
13.35 -apply (induct_tac "w")
13.36 -apply (simp_all add: number_of add_assoc [symmetric])
13.37 -done
13.38 -
13.39 -lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
13.40 -apply (induct_tac "w")
13.41 -apply (simp_all del: bin_pred_Pls bin_pred_Min bin_pred_BIT
13.42 - add: number_of number_of_succ number_of_pred add_assoc)
13.43 -done
13.44 -
13.45 -text{*This proof is complicated by the mutual recursion*}
13.46 -lemma number_of_add [rule_format]:
13.47 - "\<forall>w. number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
13.48 -apply (induct_tac "v")
13.49 -apply (simp add: number_of)
13.50 -apply (simp add: number_of number_of_pred)
13.51 -apply (rule allI)
13.52 -apply (induct_tac "w")
13.53 -apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac)
13.54 -done
13.55 -
13.56 -lemma number_of_mult:
13.57 - "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
13.58 -apply (induct_tac "v", simp add: number_of)
13.59 -apply (simp add: number_of number_of_minus)
13.60 -apply (simp add: number_of number_of_add left_distrib add_ac)
13.61 -done
13.62 -
13.63 -text{*The correctness of shifting. But it doesn't seem to give a measurable
13.64 - speed-up.*}
13.65 -lemma double_number_of_BIT:
13.66 - "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
13.67 -apply (induct_tac "w")
13.68 -apply (simp_all add: number_of number_of_add left_distrib add_ac)
13.69 -done
13.70 -
13.71 -
13.72 -text{*Converting numerals 0 and 1 to their abstract versions*}
13.73 -lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
13.74 -by (simp add: number_of)
13.75 -
13.76 -lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
13.77 -by (simp add: number_of)
13.78 -
13.79 -text{*Special-case simplification for small constants*}
13.80 -
13.81 -text{*Unary minus for the abstract constant 1. Cannot be inserted
13.82 - as a simprule until later: it is @{text number_of_Min} re-oriented!*}
13.83 -lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
13.84 -by (simp add: number_of)
13.85 -
13.86 -lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
13.87 -by (simp add: numeral_m1_eq_minus_1)
13.88 -
13.89 -lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
13.90 -by (simp add: numeral_m1_eq_minus_1)
13.91 -
13.92 -(*Negation of a coefficient*)
13.93 -lemma minus_number_of_mult [simp]:
13.94 - "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
13.95 -by (simp add: number_of_minus)
13.96 -
13.97 -text{*Subtraction*}
13.98 -lemma diff_number_of_eq:
13.99 - "number_of v - number_of w =
13.100 - (number_of(bin_add v (bin_minus w))::'a::number_ring)"
13.101 -by (simp add: diff_minus number_of_add number_of_minus)
13.102 -
13.103 -
13.104 -subsection{*Equality of Binary Numbers*}
13.105 -
13.106 -text{*First version by Norbert Voelker*}
13.107 -
13.108 -lemma eq_number_of_eq:
13.109 - "((number_of x::'a::number_ring) = number_of y) =
13.110 - iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
13.111 -by (simp add: iszero_def compare_rls number_of_add number_of_minus)
13.112 -
13.113 -lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::'a::number_ring)"
13.114 -by (simp add: iszero_def numeral_0_eq_0)
13.115 -
13.116 -lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::'a::number_ring)"
13.117 -by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
13.118 -
13.119 -
13.120 -subsection{*Comparisons, for Ordered Rings*}
13.121 -
13.122 -lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
13.123 -proof -
13.124 - have "a + a = (1+1)*a" by (simp add: left_distrib)
13.125 - with zero_less_two [where 'a = 'a]
13.126 - show ?thesis by force
13.127 -qed
13.128 -
13.129 -lemma le_imp_0_less:
13.130 - assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
13.131 -proof -
13.132 - have "0 \<le> z" .
13.133 - also have "... < z + 1" by (rule less_add_one)
13.134 - also have "... = 1 + z" by (simp add: add_ac)
13.135 - finally show "0 < 1 + z" .
13.136 -qed
13.137 -
13.138 -lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
13.139 -proof (cases z rule: int_cases)
13.140 - case (nonneg n)
13.141 - have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
13.142 - thus ?thesis using le_imp_0_less [OF le]
13.143 - by (auto simp add: add_assoc)
13.144 -next
13.145 - case (neg n)
13.146 - show ?thesis
13.147 - proof
13.148 - assume eq: "1 + z + z = 0"
13.149 - have "0 < 1 + (int n + int n)"
13.150 - by (simp add: le_imp_0_less add_increasing)
13.151 - also have "... = - (1 + z + z)"
13.152 - by (simp add: neg add_assoc [symmetric])
13.153 - also have "... = 0" by (simp add: eq)
13.154 - finally have "0<0" ..
13.155 - thus False by blast
13.156 - qed
13.157 -qed
13.158 -
13.159 -
13.160 -text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
13.161 -lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
13.162 -proof (unfold Ints_def)
13.163 - assume "a \<in> range of_int"
13.164 - then obtain z where a: "a = of_int z" ..
13.165 - show ?thesis
13.166 - proof
13.167 - assume eq: "1 + a + a = 0"
13.168 - hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
13.169 - hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
13.170 - with odd_nonzero show False by blast
13.171 - qed
13.172 -qed
13.173 -
13.174 -lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
13.175 -by (induct_tac "w", simp_all add: number_of)
13.176 -
13.177 -lemma iszero_number_of_BIT:
13.178 - "iszero (number_of (w BIT x)::'a) =
13.179 - (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
13.180 -by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff
13.181 - number_of Ints_odd_nonzero [OF Ints_number_of])
13.182 -
13.183 -lemma iszero_number_of_0:
13.184 - "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) =
13.185 - iszero (number_of w :: 'a)"
13.186 -by (simp only: iszero_number_of_BIT simp_thms)
13.187 -
13.188 -lemma iszero_number_of_1:
13.189 - "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
13.190 -by (simp only: iszero_number_of_BIT simp_thms)
13.191 -
13.192 -
13.193 -
13.194 -subsection{*The Less-Than Relation*}
13.195 -
13.196 -lemma less_number_of_eq_neg:
13.197 - "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
13.198 - = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
13.199 -apply (subst less_iff_diff_less_0)
13.200 -apply (simp add: neg_def diff_minus number_of_add number_of_minus)
13.201 -done
13.202 -
13.203 -text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
13.204 - @{term Numeral0} IS @{term "number_of Pls"} *}
13.205 -lemma not_neg_number_of_Pls:
13.206 - "~ neg (number_of bin.Pls ::'a::{ordered_idom,number_ring})"
13.207 -by (simp add: neg_def numeral_0_eq_0)
13.208 -
13.209 -lemma neg_number_of_Min:
13.210 - "neg (number_of bin.Min ::'a::{ordered_idom,number_ring})"
13.211 -by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
13.212 -
13.213 -lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
13.214 -proof -
13.215 - have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
13.216 - also have "... = (a < 0)"
13.217 - by (simp add: mult_less_0_iff zero_less_two
13.218 - order_less_not_sym [OF zero_less_two])
13.219 - finally show ?thesis .
13.220 -qed
13.221 -
13.222 -lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
13.223 -proof (cases z rule: int_cases)
13.224 - case (nonneg n)
13.225 - thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
13.226 - le_imp_0_less [THEN order_less_imp_le])
13.227 -next
13.228 - case (neg n)
13.229 - thus ?thesis by (simp del: int_Suc
13.230 - add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
13.231 -qed
13.232 -
13.233 -text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
13.234 -lemma Ints_odd_less_0:
13.235 - "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
13.236 -proof (unfold Ints_def)
13.237 - assume "a \<in> range of_int"
13.238 - then obtain z where a: "a = of_int z" ..
13.239 - hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
13.240 - by (simp add: a)
13.241 - also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
13.242 - also have "... = (a < 0)" by (simp add: a)
13.243 - finally show ?thesis .
13.244 -qed
13.245 -
13.246 -lemma neg_number_of_BIT:
13.247 - "neg (number_of (w BIT x)::'a) =
13.248 - neg (number_of w :: 'a::{ordered_idom,number_ring})"
13.249 -by (simp add: number_of neg_def double_less_0_iff
13.250 - Ints_odd_less_0 [OF Ints_number_of])
13.251 -
13.252 -
13.253 -text{*Less-Than or Equals*}
13.254 -
13.255 -text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
13.256 -lemmas le_number_of_eq_not_less =
13.257 - linorder_not_less [of "number_of w" "number_of v", symmetric,
13.258 - standard]
13.259 -
13.260 -lemma le_number_of_eq:
13.261 - "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
13.262 - = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
13.263 -by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
13.264 -
13.265 -
13.266 -text{*Absolute value (@{term abs})*}
13.267 -
13.268 -lemma abs_number_of:
13.269 - "abs(number_of x::'a::{ordered_idom,number_ring}) =
13.270 - (if number_of x < (0::'a) then -number_of x else number_of x)"
13.271 -by (simp add: abs_if)
13.272 -
13.273 -
13.274 -text{*Re-orientation of the equation nnn=x*}
13.275 -lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
13.276 -by auto
13.277 -
13.278 -
13.279 -(*Delete the original rewrites, with their clumsy conditional expressions*)
13.280 -declare bin_succ_BIT [simp del] bin_pred_BIT [simp del]
13.281 - bin_minus_BIT [simp del]
13.282 -
13.283 -declare bin_add_BIT [simp del] bin_mult_BIT [simp del]
13.284 -declare NCons_Pls [simp del] NCons_Min [simp del]
13.285 -
13.286 -(*Hide the binary representation of integer constants*)
13.287 -declare number_of_Pls [simp del] number_of_Min [simp del]
13.288 - number_of_BIT [simp del]
13.289 -
13.290 -
13.291 -
13.292 -(*Simplification of arithmetic operations on integer constants.
13.293 - Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
13.294 -
13.295 -lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
13.296 -
13.297 -lemmas bin_arith_extra_simps =
13.298 - number_of_add [symmetric]
13.299 - number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
13.300 - number_of_mult [symmetric]
13.301 - bin_succ_1 bin_succ_0
13.302 - bin_pred_1 bin_pred_0
13.303 - bin_minus_1 bin_minus_0
13.304 - bin_add_Pls_right bin_add_Min_right
13.305 - bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
13.306 - diff_number_of_eq abs_number_of abs_zero abs_one
13.307 - bin_mult_1 bin_mult_0 NCons_simps
13.308 -
13.309 -(*For making a minimal simpset, one must include these default simprules
13.310 - of thy. Also include simp_thms, or at least (~False)=True*)
13.311 -lemmas bin_arith_simps =
13.312 - bin_pred_Pls bin_pred_Min
13.313 - bin_succ_Pls bin_succ_Min
13.314 - bin_add_Pls bin_add_Min
13.315 - bin_minus_Pls bin_minus_Min
13.316 - bin_mult_Pls bin_mult_Min bin_arith_extra_simps
13.317 -
13.318 -(*Simplification of relational operations*)
13.319 -lemmas bin_rel_simps =
13.320 - eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
13.321 - iszero_number_of_0 iszero_number_of_1
13.322 - less_number_of_eq_neg
13.323 - not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
13.324 - neg_number_of_Min neg_number_of_BIT
13.325 - le_number_of_eq
13.326 -
13.327 -declare bin_arith_extra_simps [simp]
13.328 -declare bin_rel_simps [simp]
13.329 -
13.330 -
13.331 -subsection{*Simplification of arithmetic when nested to the right*}
13.332 -
13.333 -lemma add_number_of_left [simp]:
13.334 - "number_of v + (number_of w + z) =
13.335 - (number_of(bin_add v w) + z::'a::number_ring)"
13.336 -by (simp add: add_assoc [symmetric])
13.337 -
13.338 -lemma mult_number_of_left [simp]:
13.339 - "number_of v * (number_of w * z) =
13.340 - (number_of(bin_mult v w) * z::'a::number_ring)"
13.341 -by (simp add: mult_assoc [symmetric])
13.342 -
13.343 -lemma add_number_of_diff1:
13.344 - "number_of v + (number_of w - c) =
13.345 - number_of(bin_add v w) - (c::'a::number_ring)"
13.346 -by (simp add: diff_minus add_number_of_left)
13.347 -
13.348 -lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
13.349 - number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
13.350 -apply (subst diff_number_of_eq [symmetric])
13.351 -apply (simp only: compare_rls)
13.352 -done
13.353 -
13.354 -end
14.1 --- a/src/HOL/Integ/IntArith.thy Wed Jun 30 14:04:58 2004 +0200
14.2 +++ b/src/HOL/Integ/IntArith.thy Thu Jul 01 12:29:53 2004 +0200
14.3 @@ -5,7 +5,7 @@
14.4
14.5 header {* Integer arithmetic *}
14.6
14.7 -theory IntArith = Bin
14.8 +theory IntArith = Numeral
14.9 files ("int_arith1.ML"):
14.10
14.11 text{*Duplicate: can't understand why it's necessary*}
14.12 @@ -16,26 +16,12 @@
14.13 instance
14.14 int :: number ..
14.15
14.16 -primrec (*the type constraint is essential!*)
14.17 - number_of_Pls: "number_of bin.Pls = 0"
14.18 - number_of_Min: "number_of bin.Min = - (1::int)"
14.19 - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
14.20 - (number_of w) + (number_of w)"
14.21 -
14.22 -declare number_of_Pls [simp del]
14.23 - number_of_Min [simp del]
14.24 - number_of_BIT [simp del]
14.25 +defs (overloaded)
14.26 + int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)"
14.27 + --{*the type constraint is essential!*}
14.28
14.29 instance int :: number_ring
14.30 -proof
14.31 - show "Numeral0 = (0::int)" by (rule number_of_Pls)
14.32 - show "-1 = - (1::int)" by (rule number_of_Min)
14.33 - fix w :: bin and x :: bool
14.34 - show "(number_of (w BIT x) :: int) =
14.35 - (if x then 1 else 0) + number_of w + number_of w"
14.36 - by (rule number_of_BIT)
14.37 -qed
14.38 -
14.39 +by (intro_classes, simp add: int_number_of_def)
14.40
14.41
14.42 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
14.43 @@ -135,9 +121,7 @@
14.44
14.45 lemma of_int_number_of_eq:
14.46 "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
14.47 -apply (induct v)
14.48 -apply (simp_all only: number_of of_int_add, simp_all)
14.49 -done
14.50 +by (simp add: number_of_eq)
14.51
14.52 text{*Lemmas for specialist use, NOT as default simprules*}
14.53 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
14.54 @@ -210,7 +194,7 @@
14.55
14.56
14.57 (*Analogous to zadd_int*)
14.58 -lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
14.59 +lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
14.60 by (induct m n rule: diff_induct, simp_all)
14.61
14.62 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
15.1 --- a/src/HOL/Integ/IntDef.thy Wed Jun 30 14:04:58 2004 +0200
15.2 +++ b/src/HOL/Integ/IntDef.thy Thu Jul 01 12:29:53 2004 +0200
15.3 @@ -810,10 +810,9 @@
15.4 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
15.5 by (induct n, auto)
15.6
15.7 -lemma of_int_int_eq [simp]: "of_int (int n) = int n"
15.8 +lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
15.9 by (simp add: int_eq_of_nat)
15.10
15.11 -
15.12 lemma Ints_cases [case_names of_int, cases set: Ints]:
15.13 "q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C"
15.14 proof (simp add: Ints_def)
15.15 @@ -922,6 +921,12 @@
15.16 by (cases z) auto
15.17
15.18
15.19 +lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
15.20 +apply (cases z)
15.21 +apply (simp_all add: not_zle_0_negative del: int_Suc)
15.22 +done
15.23 +
15.24 +
15.25 (*Legacy ML bindings, but no longer the structure Int.*)
15.26 ML
15.27 {*
16.1 --- a/src/HOL/Integ/IntDiv.thy Wed Jun 30 14:04:58 2004 +0200
16.2 +++ b/src/HOL/Integ/IntDiv.thy Thu Jul 01 12:29:53 2004 +0200
16.3 @@ -221,7 +221,7 @@
16.4 (** Basic laws about division and remainder **)
16.5
16.6 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
16.7 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.8 +apply (case_tac "b = 0", simp)
16.9 apply (cut_tac a = a and b = b in divAlg_correct)
16.10 apply (auto simp add: quorem_def div_def mod_def)
16.11 done
16.12 @@ -302,7 +302,7 @@
16.13
16.14 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
16.15 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
16.16 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.17 +apply (case_tac "b = 0", simp)
16.18 apply (simp add: quorem_div_mod [THEN quorem_neg, simplified,
16.19 THEN quorem_div, THEN sym])
16.20
16.21 @@ -310,7 +310,7 @@
16.22
16.23 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
16.24 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
16.25 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.26 +apply (case_tac "b = 0", simp)
16.27 apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod],
16.28 auto)
16.29 done
16.30 @@ -332,7 +332,7 @@
16.31
16.32 lemma zmod_zminus1_eq_if:
16.33 "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"
16.34 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.35 +apply (case_tac "b = 0", simp)
16.36 apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod])
16.37 done
16.38
16.39 @@ -384,7 +384,7 @@
16.40
16.41 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
16.42 lemma zmod_self [simp]: "a mod a = (0::int)"
16.43 -apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
16.44 +apply (case_tac "a = 0", simp)
16.45 apply (simp add: quorem_div_mod [THEN self_remainder])
16.46 done
16.47
16.48 @@ -588,12 +588,12 @@
16.49 by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
16.50
16.51 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
16.52 -apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
16.53 +apply (case_tac "c = 0", simp)
16.54 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
16.55 done
16.56
16.57 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
16.58 -apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
16.59 +apply (case_tac "c = 0", simp)
16.60 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
16.61 done
16.62
16.63 @@ -642,22 +642,22 @@
16.64 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
16.65 lemma zdiv_zadd1_eq:
16.66 "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
16.67 -apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
16.68 +apply (case_tac "c = 0", simp)
16.69 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
16.70 done
16.71
16.72 lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
16.73 -apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
16.74 +apply (case_tac "c = 0", simp)
16.75 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
16.76 done
16.77
16.78 lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
16.79 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.80 +apply (case_tac "b = 0", simp)
16.81 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
16.82 done
16.83
16.84 lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
16.85 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.86 +apply (case_tac "b = 0", simp)
16.87 apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
16.88 done
16.89
16.90 @@ -680,12 +680,12 @@
16.91 by (simp add: zdiv_zadd1_eq)
16.92
16.93 lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
16.94 -apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
16.95 +apply (case_tac "a = 0", simp)
16.96 apply (simp add: zmod_zadd1_eq)
16.97 done
16.98
16.99 lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
16.100 -apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
16.101 +apply (case_tac "a = 0", simp)
16.102 apply (simp add: zmod_zadd1_eq)
16.103 done
16.104
16.105 @@ -737,13 +737,13 @@
16.106 zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
16.107
16.108 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
16.109 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.110 +apply (case_tac "b = 0", simp)
16.111 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div])
16.112 done
16.113
16.114 lemma zmod_zmult2_eq:
16.115 "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
16.116 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.117 +apply (case_tac "b = 0", simp)
16.118 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod])
16.119 done
16.120
16.121 @@ -759,7 +759,7 @@
16.122 done
16.123
16.124 lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b"
16.125 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.126 +apply (case_tac "b = 0", simp)
16.127 apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
16.128 done
16.129
16.130 @@ -781,8 +781,8 @@
16.131 done
16.132
16.133 lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
16.134 -apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
16.135 -apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
16.136 +apply (case_tac "b = 0", simp)
16.137 +apply (case_tac "c = 0", simp)
16.138 apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
16.139 done
16.140
16.141 @@ -832,7 +832,7 @@
16.142 (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
16.143 (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
16.144 apply (case_tac "k=0")
16.145 - apply (simp add: DIVISION_BY_ZERO)
16.146 + apply (simp)
16.147 apply (simp only: linorder_neq_iff)
16.148 apply (erule disjE)
16.149 apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
16.150 @@ -845,7 +845,7 @@
16.151 (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
16.152 (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
16.153 apply (case_tac "k=0")
16.154 - apply (simp add: DIVISION_BY_ZERO)
16.155 + apply (simp)
16.156 apply (simp only: linorder_neq_iff)
16.157 apply (erule disjE)
16.158 apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
16.159 @@ -904,20 +904,16 @@
16.160 (if ~b | (0::int) \<le> number_of w
16.161 then number_of v div (number_of w)
16.162 else (number_of v + (1::int)) div (number_of w))"
16.163 -apply (simp only: add_assoc number_of_BIT)
16.164 -(*create subgoal because the next step can't simplify numerals*)
16.165 -apply (subgoal_tac "2 ~= (0::int) ")
16.166 -apply (simp del: bin_arith_extra_simps arith_special
16.167 - add: zdiv_zmult_zmult1 pos_zdiv_mult_2 not_0_le_lemma neg_zdiv_mult_2)
16.168 -apply simp
16.169 +apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if)
16.170 +apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
16.171 done
16.172
16.173
16.174 -(** computing mod by shifting (proofs resemble those for div) **)
16.175 +subsection{*Computing mod by Shifting (proofs resemble those for div)*}
16.176
16.177 lemma pos_zmod_mult_2:
16.178 "(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
16.179 -apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
16.180 +apply (case_tac "a = 0", simp)
16.181 apply (subgoal_tac "1 \<le> a")
16.182 prefer 2 apply arith
16.183 apply (subgoal_tac "1 < a * 2")
16.184 @@ -952,15 +948,14 @@
16.185 then 2 * (number_of v mod number_of w) + 1
16.186 else 2 * ((number_of v + (1::int)) mod number_of w) - 1
16.187 else 2 * (number_of v mod number_of w))"
16.188 -apply (simp only: zadd_assoc number_of_BIT)
16.189 -apply (simp del: bin_arith_extra_simps bin_rel_simps arith_special
16.190 - add: zmod_zmult_zmult1 pos_zmod_mult_2 not_0_le_lemma neg_zmod_mult_2
16.191 - neg_def)
16.192 +apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if)
16.193 +apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
16.194 + not_0_le_lemma neg_zmod_mult_2 add_ac)
16.195 done
16.196
16.197
16.198
16.199 -(** Quotients of signs **)
16.200 +subsection{*Quotients of Signs*}
16.201
16.202 lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"
16.203 apply (subgoal_tac "a div b \<le> -1", force)
17.1 --- a/src/HOL/Integ/NatBin.thy Wed Jun 30 14:04:58 2004 +0200
17.2 +++ b/src/HOL/Integ/NatBin.thy Thu Jul 01 12:29:53 2004 +0200
17.3 @@ -478,8 +478,8 @@
17.4
17.5
17.6 lemma eq_number_of_BIT_Pls:
17.7 - "((number_of (v BIT x) ::int) = number_of bin.Pls) =
17.8 - (x=False & (((number_of v) ::int) = number_of bin.Pls))"
17.9 + "((number_of (v BIT x) ::int) = Numeral0) =
17.10 + (x=False & (((number_of v) ::int) = Numeral0))"
17.11 apply (simp only: simp_thms add: number_of_BIT number_of_Pls eq_commute
17.12 split add: split_if cong: imp_cong)
17.13 apply (rule_tac x = "number_of v" in spec, safe)
17.14 @@ -489,15 +489,15 @@
17.15 done
17.16
17.17 lemma eq_number_of_BIT_Min:
17.18 - "((number_of (v BIT x) ::int) = number_of bin.Min) =
17.19 - (x=True & (((number_of v) ::int) = number_of bin.Min))"
17.20 + "((number_of (v BIT x) ::int) = number_of Numeral.Min) =
17.21 + (x=True & (((number_of v) ::int) = number_of Numeral.Min))"
17.22 apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute
17.23 split add: split_if cong: imp_cong)
17.24 apply (rule_tac x = "number_of v" in spec, auto)
17.25 apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
17.26 done
17.27
17.28 -lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min"
17.29 +lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Numeral.Min"
17.30 by auto
17.31
17.32
17.33 @@ -569,10 +569,10 @@
17.34 declare split_div[of _ _ "number_of k", standard, arith_split]
17.35 declare split_mod[of _ _ "number_of k", standard, arith_split]
17.36
17.37 -lemma nat_number_of_Pls: "number_of bin.Pls = (0::nat)"
17.38 +lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
17.39 by (simp add: number_of_Pls nat_number_of_def)
17.40
17.41 -lemma nat_number_of_Min: "number_of bin.Min = (0::nat)"
17.42 +lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
17.43 apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
17.44 apply (simp add: neg_nat)
17.45 done
17.46 @@ -622,23 +622,12 @@
17.47 lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
17.48 by (simp only: nat_number_of_def, simp)
17.49
17.50 -lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
17.51 -by arith
17.52 -
17.53 lemma of_nat_number_of_lemma:
17.54 "of_nat (number_of v :: nat) =
17.55 (if 0 \<le> (number_of v :: int)
17.56 then (number_of v :: 'a :: number_ring)
17.57 else 0)"
17.58 -apply (induct v, simp, simp add: nat_numeral_m1_eq_0)
17.59 -apply (simp only: number_of nat_number_of_def)
17.60 -txt{*Generalize in order to eliminate the function @{term number_of} and
17.61 -its annoying simprules*}
17.62 -apply (erule rev_mp)
17.63 -apply (rule_tac x="number_of bin :: int" in spec)
17.64 -apply (rule_tac x="number_of bin :: 'a" in spec)
17.65 -apply (simp add: nat_add_distrib of_nat_double int_double_iff)
17.66 -done
17.67 +by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
17.68
17.69 lemma of_nat_number_of_eq [simp]:
17.70 "of_nat (number_of v :: nat) =
17.71 @@ -850,6 +839,8 @@
17.72 "uminus" :: "int => int" ("`~")
17.73 "op +" :: "int => int => int" ("(_ `+/ _)")
17.74 "op *" :: "int => int => int" ("(_ `*/ _)")
17.75 + "op div" :: "int => int => int" ("(_ `div/ _)")
17.76 + "op mod" :: "int => int => int" ("(_ `mod/ _)")
17.77 "op <" :: "int => int => bool" ("(_ </ _)")
17.78 "op <=" :: "int => int => bool" ("(_ <=/ _)")
17.79 "neg" ("(_ < 0)")
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/Integ/Numeral.thy Thu Jul 01 12:29:53 2004 +0200
18.3 @@ -0,0 +1,505 @@
18.4 +(* Title: HOL/Integ/Numeral.thy
18.5 + ID: $Id$
18.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
18.7 + Copyright 1994 University of Cambridge
18.8 +*)
18.9 +
18.10 +header{*Arithmetic on Binary Integers*}
18.11 +
18.12 +theory Numeral = IntDef
18.13 +files "Tools/numeral_syntax.ML":
18.14 +
18.15 +text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
18.16 + Only qualified access Numeral.Pls and Numeral.Min is allowed.
18.17 + We do not hide Bit because we need the BIT infix syntax.*}
18.18 +
18.19 +text{*This formalization defines binary arithmetic in terms of the integers
18.20 +rather than using a datatype. This avoids multiple representations (leading
18.21 +zeroes, etc.) See @{text "ZF/Integ/twos-compl.ML"}, function @{text
18.22 +int_of_binary}, for the numerical interpretation.
18.23 +
18.24 +The representation expects that @{text "(m mod 2)"} is 0 or 1,
18.25 +even if m is negative;
18.26 +For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
18.27 +@{text "-5 = (-3)*2 + 1"}.
18.28 +*}
18.29 +
18.30 +
18.31 +typedef (Bin)
18.32 + bin = "UNIV::int set"
18.33 + by (auto)
18.34 +
18.35 +constdefs
18.36 + Pls :: "bin"
18.37 + "Pls == Abs_Bin 0"
18.38 +
18.39 + Min :: "bin"
18.40 + "Min == Abs_Bin (- 1)"
18.41 +
18.42 + Bit :: "[bin,bool] => bin" (infixl "BIT" 90)
18.43 + --{*That is, 2w+b*}
18.44 + "w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
18.45 +
18.46 +
18.47 +axclass
18.48 + number < type -- {* for numeric types: nat, int, real, \dots *}
18.49 +
18.50 +consts
18.51 + number_of :: "bin => 'a::number"
18.52 +
18.53 +syntax
18.54 + "_Numeral" :: "num_const => 'a" ("_")
18.55 + Numeral0 :: 'a
18.56 + Numeral1 :: 'a
18.57 +
18.58 +translations
18.59 + "Numeral0" == "number_of Numeral.Pls"
18.60 + "Numeral1" == "number_of (Numeral.Pls BIT True)"
18.61 +
18.62 +
18.63 +setup NumeralSyntax.setup
18.64 +
18.65 +syntax (xsymbols)
18.66 + "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
18.67 +syntax (HTML output)
18.68 + "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
18.69 +syntax (output)
18.70 + "_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
18.71 +translations
18.72 + "x\<twosuperior>" == "x^2"
18.73 + "x\<twosuperior>" <= "x^(2::nat)"
18.74 +
18.75 +
18.76 +lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
18.77 + -- {* Unfold all @{text let}s involving constants *}
18.78 + by (simp add: Let_def)
18.79 +
18.80 +lemma Let_0 [simp]: "Let 0 f == f 0"
18.81 + by (simp add: Let_def)
18.82 +
18.83 +lemma Let_1 [simp]: "Let 1 f == f 1"
18.84 + by (simp add: Let_def)
18.85 +
18.86 +
18.87 +constdefs
18.88 + bin_succ :: "bin=>bin"
18.89 + "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
18.90 +
18.91 + bin_pred :: "bin=>bin"
18.92 + "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
18.93 +
18.94 + bin_minus :: "bin=>bin"
18.95 + "bin_minus w == Abs_Bin(- (Rep_Bin w))"
18.96 +
18.97 + bin_add :: "[bin,bin]=>bin"
18.98 + "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
18.99 +
18.100 + bin_mult :: "[bin,bin]=>bin"
18.101 + "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
18.102 +
18.103 +
18.104 +lemmas Bin_simps =
18.105 + bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
18.106 + Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
18.107 +
18.108 +text{*Removal of leading zeroes*}
18.109 +lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
18.110 +by (simp add: Bin_simps)
18.111 +
18.112 +lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
18.113 +by (simp add: Bin_simps)
18.114 +
18.115 +subsection{*The Functions @{term bin_succ}, @{term bin_pred} and @{term bin_minus}*}
18.116 +
18.117 +lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
18.118 +by (simp add: Bin_simps)
18.119 +
18.120 +lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
18.121 +by (simp add: Bin_simps)
18.122 +
18.123 +lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
18.124 +by (simp add: Bin_simps add_ac)
18.125 +
18.126 +lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
18.127 +by (simp add: Bin_simps add_ac)
18.128 +
18.129 +lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
18.130 +by (simp add: Bin_simps)
18.131 +
18.132 +lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
18.133 +by (simp add: Bin_simps diff_minus)
18.134 +
18.135 +lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
18.136 +by (simp add: Bin_simps)
18.137 +
18.138 +lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
18.139 +by (simp add: Bin_simps diff_minus add_ac)
18.140 +
18.141 +lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
18.142 +by (simp add: Bin_simps)
18.143 +
18.144 +lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
18.145 +by (simp add: Bin_simps)
18.146 +
18.147 +lemma bin_minus_1 [simp]:
18.148 + "bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
18.149 +by (simp add: Bin_simps add_ac diff_minus)
18.150 +
18.151 + lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
18.152 +by (simp add: Bin_simps)
18.153 +
18.154 +
18.155 +subsection{*Binary Addition and Multiplication:
18.156 + @{term bin_add} and @{term bin_mult}*}
18.157 +
18.158 +lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
18.159 +by (simp add: Bin_simps)
18.160 +
18.161 +lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
18.162 +by (simp add: Bin_simps diff_minus add_ac)
18.163 +
18.164 +lemma bin_add_BIT_11 [simp]:
18.165 + "bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
18.166 +by (simp add: Bin_simps add_ac)
18.167 +
18.168 +lemma bin_add_BIT_10 [simp]:
18.169 + "bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
18.170 +by (simp add: Bin_simps add_ac)
18.171 +
18.172 +lemma bin_add_BIT_0 [simp]:
18.173 + "bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
18.174 +by (simp add: Bin_simps add_ac)
18.175 +
18.176 +lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
18.177 +by (simp add: Bin_simps)
18.178 +
18.179 +lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
18.180 +by (simp add: Bin_simps diff_minus)
18.181 +
18.182 +lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
18.183 +by (simp add: Bin_simps)
18.184 +
18.185 +lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
18.186 +by (simp add: Bin_simps)
18.187 +
18.188 +lemma bin_mult_1 [simp]:
18.189 + "bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
18.190 +by (simp add: Bin_simps add_ac left_distrib)
18.191 +
18.192 +lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
18.193 +by (simp add: Bin_simps left_distrib)
18.194 +
18.195 +
18.196 +
18.197 +subsection{*Converting Numerals to Rings: @{term number_of}*}
18.198 +
18.199 +axclass number_ring \<subseteq> number, comm_ring_1
18.200 + number_of_eq: "number_of w = of_int (Rep_Bin w)"
18.201 +
18.202 +lemma number_of_succ:
18.203 + "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
18.204 +by (simp add: number_of_eq Bin_simps)
18.205 +
18.206 +lemma number_of_pred:
18.207 + "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
18.208 +by (simp add: number_of_eq Bin_simps)
18.209 +
18.210 +lemma number_of_minus:
18.211 + "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
18.212 +by (simp add: number_of_eq Bin_simps)
18.213 +
18.214 +lemma number_of_add:
18.215 + "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
18.216 +by (simp add: number_of_eq Bin_simps)
18.217 +
18.218 +lemma number_of_mult:
18.219 + "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
18.220 +by (simp add: number_of_eq Bin_simps)
18.221 +
18.222 +text{*The correctness of shifting. But it doesn't seem to give a measurable
18.223 + speed-up.*}
18.224 +lemma double_number_of_BIT:
18.225 + "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
18.226 +by (simp add: number_of_eq Bin_simps left_distrib)
18.227 +
18.228 +text{*Converting numerals 0 and 1 to their abstract versions*}
18.229 +lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
18.230 +by (simp add: number_of_eq Bin_simps)
18.231 +
18.232 +lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
18.233 +by (simp add: number_of_eq Bin_simps)
18.234 +
18.235 +text{*Special-case simplification for small constants*}
18.236 +
18.237 +text{*Unary minus for the abstract constant 1. Cannot be inserted
18.238 + as a simprule until later: it is @{text number_of_Min} re-oriented!*}
18.239 +lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
18.240 +by (simp add: number_of_eq Bin_simps)
18.241 +
18.242 +
18.243 +lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
18.244 +by (simp add: numeral_m1_eq_minus_1)
18.245 +
18.246 +lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
18.247 +by (simp add: numeral_m1_eq_minus_1)
18.248 +
18.249 +(*Negation of a coefficient*)
18.250 +lemma minus_number_of_mult [simp]:
18.251 + "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
18.252 +by (simp add: number_of_minus)
18.253 +
18.254 +text{*Subtraction*}
18.255 +lemma diff_number_of_eq:
18.256 + "number_of v - number_of w =
18.257 + (number_of(bin_add v (bin_minus w))::'a::number_ring)"
18.258 +by (simp add: diff_minus number_of_add number_of_minus)
18.259 +
18.260 +
18.261 +lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
18.262 +by (simp add: number_of_eq Bin_simps)
18.263 +
18.264 +lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
18.265 +by (simp add: number_of_eq Bin_simps)
18.266 +
18.267 +lemma number_of_BIT:
18.268 + "number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
18.269 + (number_of w) + (number_of w)"
18.270 +by (simp add: number_of_eq Bin_simps)
18.271 +
18.272 +
18.273 +
18.274 +subsection{*Equality of Binary Numbers*}
18.275 +
18.276 +text{*First version by Norbert Voelker*}
18.277 +
18.278 +lemma eq_number_of_eq:
18.279 + "((number_of x::'a::number_ring) = number_of y) =
18.280 + iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
18.281 +by (simp add: iszero_def compare_rls number_of_add number_of_minus)
18.282 +
18.283 +lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
18.284 +by (simp add: iszero_def numeral_0_eq_0)
18.285 +
18.286 +lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
18.287 +by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
18.288 +
18.289 +
18.290 +subsection{*Comparisons, for Ordered Rings*}
18.291 +
18.292 +lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
18.293 +proof -
18.294 + have "a + a = (1+1)*a" by (simp add: left_distrib)
18.295 + with zero_less_two [where 'a = 'a]
18.296 + show ?thesis by force
18.297 +qed
18.298 +
18.299 +lemma le_imp_0_less:
18.300 + assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
18.301 +proof -
18.302 + have "0 \<le> z" .
18.303 + also have "... < z + 1" by (rule less_add_one)
18.304 + also have "... = 1 + z" by (simp add: add_ac)
18.305 + finally show "0 < 1 + z" .
18.306 +qed
18.307 +
18.308 +lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
18.309 +proof (cases z rule: int_cases)
18.310 + case (nonneg n)
18.311 + have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
18.312 + thus ?thesis using le_imp_0_less [OF le]
18.313 + by (auto simp add: add_assoc)
18.314 +next
18.315 + case (neg n)
18.316 + show ?thesis
18.317 + proof
18.318 + assume eq: "1 + z + z = 0"
18.319 + have "0 < 1 + (int n + int n)"
18.320 + by (simp add: le_imp_0_less add_increasing)
18.321 + also have "... = - (1 + z + z)"
18.322 + by (simp add: neg add_assoc [symmetric])
18.323 + also have "... = 0" by (simp add: eq)
18.324 + finally have "0<0" ..
18.325 + thus False by blast
18.326 + qed
18.327 +qed
18.328 +
18.329 +
18.330 +text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
18.331 +lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
18.332 +proof (unfold Ints_def)
18.333 + assume "a \<in> range of_int"
18.334 + then obtain z where a: "a = of_int z" ..
18.335 + show ?thesis
18.336 + proof
18.337 + assume eq: "1 + a + a = 0"
18.338 + hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
18.339 + hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
18.340 + with odd_nonzero show False by blast
18.341 + qed
18.342 +qed
18.343 +
18.344 +lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
18.345 +by (simp add: number_of_eq Ints_def)
18.346 +
18.347 +
18.348 +lemma iszero_number_of_BIT:
18.349 + "iszero (number_of (w BIT x)::'a) =
18.350 + (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
18.351 +by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff
18.352 + Ints_odd_nonzero Ints_def)
18.353 +
18.354 +lemma iszero_number_of_0:
18.355 + "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) =
18.356 + iszero (number_of w :: 'a)"
18.357 +by (simp only: iszero_number_of_BIT simp_thms)
18.358 +
18.359 +lemma iszero_number_of_1:
18.360 + "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
18.361 +by (simp only: iszero_number_of_BIT simp_thms)
18.362 +
18.363 +
18.364 +
18.365 +subsection{*The Less-Than Relation*}
18.366 +
18.367 +lemma less_number_of_eq_neg:
18.368 + "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
18.369 + = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
18.370 +apply (subst less_iff_diff_less_0)
18.371 +apply (simp add: neg_def diff_minus number_of_add number_of_minus)
18.372 +done
18.373 +
18.374 +text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
18.375 + @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
18.376 +lemma not_neg_number_of_Pls:
18.377 + "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
18.378 +by (simp add: neg_def numeral_0_eq_0)
18.379 +
18.380 +lemma neg_number_of_Min:
18.381 + "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
18.382 +by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
18.383 +
18.384 +lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
18.385 +proof -
18.386 + have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
18.387 + also have "... = (a < 0)"
18.388 + by (simp add: mult_less_0_iff zero_less_two
18.389 + order_less_not_sym [OF zero_less_two])
18.390 + finally show ?thesis .
18.391 +qed
18.392 +
18.393 +lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
18.394 +proof (cases z rule: int_cases)
18.395 + case (nonneg n)
18.396 + thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
18.397 + le_imp_0_less [THEN order_less_imp_le])
18.398 +next
18.399 + case (neg n)
18.400 + thus ?thesis by (simp del: int_Suc
18.401 + add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
18.402 +qed
18.403 +
18.404 +text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
18.405 +lemma Ints_odd_less_0:
18.406 + "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
18.407 +proof (unfold Ints_def)
18.408 + assume "a \<in> range of_int"
18.409 + then obtain z where a: "a = of_int z" ..
18.410 + hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
18.411 + by (simp add: a)
18.412 + also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
18.413 + also have "... = (a < 0)" by (simp add: a)
18.414 + finally show ?thesis .
18.415 +qed
18.416 +
18.417 +lemma neg_number_of_BIT:
18.418 + "neg (number_of (w BIT x)::'a) =
18.419 + neg (number_of w :: 'a::{ordered_idom,number_ring})"
18.420 +by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
18.421 + Ints_odd_less_0 Ints_def)
18.422 +
18.423 +
18.424 +text{*Less-Than or Equals*}
18.425 +
18.426 +text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
18.427 +lemmas le_number_of_eq_not_less =
18.428 + linorder_not_less [of "number_of w" "number_of v", symmetric,
18.429 + standard]
18.430 +
18.431 +lemma le_number_of_eq:
18.432 + "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
18.433 + = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
18.434 +by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
18.435 +
18.436 +
18.437 +text{*Absolute value (@{term abs})*}
18.438 +
18.439 +lemma abs_number_of:
18.440 + "abs(number_of x::'a::{ordered_idom,number_ring}) =
18.441 + (if number_of x < (0::'a) then -number_of x else number_of x)"
18.442 +by (simp add: abs_if)
18.443 +
18.444 +
18.445 +text{*Re-orientation of the equation nnn=x*}
18.446 +lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
18.447 +by auto
18.448 +
18.449 +
18.450 +
18.451 +
18.452 +subsection{*Simplification of arithmetic operations on integer constants.*}
18.453 +
18.454 +lemmas bin_arith_extra_simps =
18.455 + number_of_add [symmetric]
18.456 + number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
18.457 + number_of_mult [symmetric]
18.458 + diff_number_of_eq abs_number_of
18.459 +
18.460 +text{*For making a minimal simpset, one must include these default simprules.
18.461 + Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
18.462 +lemmas bin_arith_simps =
18.463 + Pls_0_eq Min_1_eq
18.464 + bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
18.465 + bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
18.466 + bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
18.467 + bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
18.468 + bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
18.469 + bin_add_Pls_right bin_add_Min_right
18.470 + abs_zero abs_one bin_arith_extra_simps
18.471 +
18.472 +text{*Simplification of relational operations*}
18.473 +lemmas bin_rel_simps =
18.474 + eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
18.475 + iszero_number_of_0 iszero_number_of_1
18.476 + less_number_of_eq_neg
18.477 + not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
18.478 + neg_number_of_Min neg_number_of_BIT
18.479 + le_number_of_eq
18.480 +
18.481 +declare bin_arith_extra_simps [simp]
18.482 +declare bin_rel_simps [simp]
18.483 +
18.484 +
18.485 +subsection{*Simplification of arithmetic when nested to the right*}
18.486 +
18.487 +lemma add_number_of_left [simp]:
18.488 + "number_of v + (number_of w + z) =
18.489 + (number_of(bin_add v w) + z::'a::number_ring)"
18.490 +by (simp add: add_assoc [symmetric])
18.491 +
18.492 +lemma mult_number_of_left [simp]:
18.493 + "number_of v * (number_of w * z) =
18.494 + (number_of(bin_mult v w) * z::'a::number_ring)"
18.495 +by (simp add: mult_assoc [symmetric])
18.496 +
18.497 +lemma add_number_of_diff1:
18.498 + "number_of v + (number_of w - c) =
18.499 + number_of(bin_add v w) - (c::'a::number_ring)"
18.500 +by (simp add: diff_minus add_number_of_left)
18.501 +
18.502 +lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
18.503 + number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
18.504 +apply (subst diff_number_of_eq [symmetric])
18.505 +apply (simp only: compare_rls)
18.506 +done
18.507 +
18.508 +end
19.1 --- a/src/HOL/Integ/Presburger.thy Wed Jun 30 14:04:58 2004 +0200
19.2 +++ b/src/HOL/Integ/Presburger.thy Thu Jul 01 12:29:53 2004 +0200
19.3 @@ -969,7 +969,7 @@
19.4 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
19.5 by simp
19.6
19.7 -theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
19.8 +theorem number_of2: "(0::int) <= Numeral0" by simp
19.9
19.10 theorem Suc_plus1: "Suc n = n + 1" by simp
19.11
20.1 --- a/src/HOL/Integ/int_arith1.ML Wed Jun 30 14:04:58 2004 +0200
20.2 +++ b/src/HOL/Integ/int_arith1.ML Thu Jul 01 12:29:53 2004 +0200
20.3 @@ -7,49 +7,37 @@
20.4
20.5 (** Misc ML bindings **)
20.6
20.7 -val NCons_Pls = thm"NCons_Pls";
20.8 -val NCons_Min = thm"NCons_Min";
20.9 -val NCons_BIT = thm"NCons_BIT";
20.10 -val number_of_Pls = thm"number_of_Pls";
20.11 -val number_of_Min = thm"number_of_Min";
20.12 -val number_of_BIT = thm"number_of_BIT";
20.13 val bin_succ_Pls = thm"bin_succ_Pls";
20.14 val bin_succ_Min = thm"bin_succ_Min";
20.15 -val bin_succ_BIT = thm"bin_succ_BIT";
20.16 +val bin_succ_1 = thm"bin_succ_1";
20.17 +val bin_succ_0 = thm"bin_succ_0";
20.18 +
20.19 val bin_pred_Pls = thm"bin_pred_Pls";
20.20 val bin_pred_Min = thm"bin_pred_Min";
20.21 -val bin_pred_BIT = thm"bin_pred_BIT";
20.22 +val bin_pred_1 = thm"bin_pred_1";
20.23 +val bin_pred_0 = thm"bin_pred_0";
20.24 +
20.25 val bin_minus_Pls = thm"bin_minus_Pls";
20.26 val bin_minus_Min = thm"bin_minus_Min";
20.27 -val bin_minus_BIT = thm"bin_minus_BIT";
20.28 +val bin_minus_1 = thm"bin_minus_1";
20.29 +val bin_minus_0 = thm"bin_minus_0";
20.30 +
20.31 val bin_add_Pls = thm"bin_add_Pls";
20.32 val bin_add_Min = thm"bin_add_Min";
20.33 -val bin_mult_Pls = thm"bin_mult_Pls";
20.34 -val bin_mult_Min = thm"bin_mult_Min";
20.35 -val bin_mult_BIT = thm"bin_mult_BIT";
20.36 -
20.37 -val neg_def = thm "neg_def";
20.38 -val iszero_def = thm "iszero_def";
20.39 -
20.40 -val NCons_Pls_0 = thm"NCons_Pls_0";
20.41 -val NCons_Pls_1 = thm"NCons_Pls_1";
20.42 -val NCons_Min_0 = thm"NCons_Min_0";
20.43 -val NCons_Min_1 = thm"NCons_Min_1";
20.44 -val bin_succ_1 = thm"bin_succ_1";
20.45 -val bin_succ_0 = thm"bin_succ_0";
20.46 -val bin_pred_1 = thm"bin_pred_1";
20.47 -val bin_pred_0 = thm"bin_pred_0";
20.48 -val bin_minus_1 = thm"bin_minus_1";
20.49 -val bin_minus_0 = thm"bin_minus_0";
20.50 val bin_add_BIT_11 = thm"bin_add_BIT_11";
20.51 val bin_add_BIT_10 = thm"bin_add_BIT_10";
20.52 val bin_add_BIT_0 = thm"bin_add_BIT_0";
20.53 val bin_add_Pls_right = thm"bin_add_Pls_right";
20.54 val bin_add_Min_right = thm"bin_add_Min_right";
20.55 -val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
20.56 +
20.57 +val bin_mult_Pls = thm"bin_mult_Pls";
20.58 +val bin_mult_Min = thm"bin_mult_Min";
20.59 val bin_mult_1 = thm"bin_mult_1";
20.60 val bin_mult_0 = thm"bin_mult_0";
20.61 -val number_of_NCons = thm"number_of_NCons";
20.62 +
20.63 +val neg_def = thm "neg_def";
20.64 +val iszero_def = thm "iszero_def";
20.65 +
20.66 val number_of_succ = thm"number_of_succ";
20.67 val number_of_pred = thm"number_of_pred";
20.68 val number_of_minus = thm"number_of_minus";
20.69 @@ -86,7 +74,6 @@
20.70 val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
20.71 val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
20.72
20.73 -val NCons_simps = thms"NCons_simps";
20.74 val bin_arith_extra_simps = thms"bin_arith_extra_simps";
20.75 val bin_arith_simps = thms"bin_arith_simps";
20.76 val bin_rel_simps = thms"bin_rel_simps";
20.77 @@ -298,10 +285,9 @@
20.78 bin_simps \\ [add_number_of_left, number_of_add RS sym];
20.79
20.80 (*To evaluate binary negations of coefficients*)
20.81 -val minus_simps = NCons_simps @
20.82 - [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
20.83 - bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
20.84 - bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
20.85 +val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
20.86 + bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
20.87 + bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
20.88
20.89 (*To let us treat subtraction as addition*)
20.90 val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
20.91 @@ -335,10 +321,10 @@
20.92 val find_first_coeff = find_first_coeff []
20.93 val trans_tac = trans_tac
20.94 val norm_tac =
20.95 - ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
20.96 + ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
20.97 diff_simps@minus_simps@add_ac))
20.98 - THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
20.99 - THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
20.100 + THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
20.101 + THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
20.102 add_ac@mult_ac))
20.103 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
20.104 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
20.105 @@ -411,10 +397,10 @@
20.106 val prove_conv = Bin_Simprocs.prove_conv_nohyps
20.107 val trans_tac = trans_tac
20.108 val norm_tac =
20.109 - ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
20.110 + ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
20.111 diff_simps@minus_simps@add_ac))
20.112 - THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
20.113 - THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
20.114 + THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
20.115 + THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
20.116 add_ac@mult_ac))
20.117 val numeral_simp_tac = ALLGOALS
20.118 (simp_tac (HOL_ss addsimps add_0s@bin_simps))
21.1 --- a/src/HOL/Integ/presburger.ML Wed Jun 30 14:04:58 2004 +0200
21.2 +++ b/src/HOL/Integ/presburger.ML Thu Jul 01 12:29:53 2004 +0200
21.3 @@ -120,9 +120,9 @@
21.4 ("HOL.max", nT --> nT --> nT),
21.5 ("HOL.min", nT --> nT --> nT),
21.6
21.7 - ("Numeral.bin.Bit", binT --> bT --> binT),
21.8 - ("Numeral.bin.Pls", binT),
21.9 - ("Numeral.bin.Min", binT),
21.10 + ("Numeral.Bit", binT --> bT --> binT),
21.11 + ("Numeral.Pls", binT),
21.12 + ("Numeral.Min", binT),
21.13 ("Numeral.number_of", binT --> iT),
21.14 ("Numeral.number_of", binT --> nT),
21.15 ("0", nT),
22.1 --- a/src/HOL/IsaMakefile Wed Jun 30 14:04:58 2004 +0200
22.2 +++ b/src/HOL/IsaMakefile Thu Jul 01 12:29:53 2004 +0200
22.3 @@ -84,14 +84,14 @@
22.4 Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
22.5 Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
22.6 Fun.thy Gfp.ML Gfp.thy Hilbert_Choice.thy HOL.ML \
22.7 - HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Bin.thy \
22.8 + HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
22.9 Integ/cooper_dec.ML Integ/cooper_proof.ML \
22.10 Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
22.11 Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
22.12 Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
22.13 Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
22.14 Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
22.15 - Nat.thy NatArith.ML NatArith.thy Numeral.thy \
22.16 + Nat.thy NatArith.ML NatArith.thy \
22.17 Power.thy PreList.thy Product_Type.ML Product_Type.thy \
22.18 Refute.thy ROOT.ML \
22.19 Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
23.1 --- a/src/HOL/Library/Word.thy Wed Jun 30 14:04:58 2004 +0200
23.2 +++ b/src/HOL/Library/Word.thy Thu Jul 01 12:29:53 2004 +0200
23.3 @@ -378,13 +378,14 @@
23.4
23.5 constdefs
23.6 bv_to_nat :: "bit list => int"
23.7 - "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bv)"
23.8 + "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bv)"
23.9
23.10 lemma [simp]: "bv_to_nat [] = 0"
23.11 by (simp add: bv_to_nat_def)
23.12
23.13 -lemma pos_number_of: "(0::int)\<le> number_of w ==> number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
23.14 - by (induct w,auto,simp add: iszero_def)
23.15 +lemma pos_number_of:
23.16 + "number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
23.17 +by (simp add: mult_2)
23.18
23.19 lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
23.20 proof -
23.21 @@ -393,26 +394,24 @@
23.22 by (simp add: bv_to_nat'_def)
23.23 have [rule_format]: "\<forall> base bs. (0::int) \<le> number_of base --> (\<forall> b. bv_to_nat' base (b # bs) = bv_to_nat' (base BIT (b = \<one>)) bs)"
23.24 by (simp add: bv_to_nat'_def)
23.25 - have helper [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' bin.Pls bs"
23.26 + have helper [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' Numeral.Pls bs"
23.27 proof (induct bs,simp add: bv_to_nat'_def,clarify)
23.28 fix x xs base
23.29 - assume ind [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' bin.Pls xs"
23.30 + assume ind [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' Numeral.Pls xs"
23.31 assume base_pos: "(0::int) \<le> number_of base"
23.32 def qq == "number_of base::int"
23.33 - show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' bin.Pls (x # xs)"
23.34 + show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' Numeral.Pls (x # xs)"
23.35 apply (unfold bv_to_nat'_def)
23.36 apply (simp only: foldl.simps)
23.37 apply (fold bv_to_nat'_def)
23.38 apply (subst ind [of "base BIT (x = \<one>)"])
23.39 using base_pos
23.40 apply simp
23.41 - apply (subst ind [of "bin.Pls BIT (x = \<one>)"])
23.42 + apply (subst ind [of "Numeral.Pls BIT (x = \<one>)"])
23.43 apply simp
23.44 apply (subst pos_number_of [of "base" "x = \<one>"])
23.45 using base_pos
23.46 - apply simp
23.47 - apply (subst pos_number_of [of "bin.Pls" "x = \<one>"])
23.48 - apply simp
23.49 + apply (subst pos_number_of [of "Numeral.Pls" "x = \<one>"])
23.50 apply (fold qq_def)
23.51 apply (simp add: ring_distrib)
23.52 done
23.53 @@ -2859,14 +2858,15 @@
23.54
23.55 lemmas [simp] = length_nat_non0
23.56
23.57 -lemma "nat_to_bv (number_of bin.Pls) = []"
23.58 +lemma "nat_to_bv (number_of Numeral.Pls) = []"
23.59 by simp
23.60
23.61 +(***NO LONGER WORKS
23.62 consts
23.63 fast_nat_to_bv_helper :: "bin => bit list => bit list"
23.64
23.65 primrec
23.66 - fast_nat_to_bv_Pls: "fast_nat_to_bv_helper bin.Pls res = res"
23.67 + fast_nat_to_bv_Pls: "fast_nat_to_bv_helper Numeral.Pls res = res"
23.68 fast_nat_to_bv_Bit: "fast_nat_to_bv_helper (w BIT b) res = fast_nat_to_bv_helper w ((if b then \<one> else \<zero>) # res)"
23.69
23.70 lemma fast_nat_to_bv_def:
23.71 @@ -2889,7 +2889,7 @@
23.72 by (simp add: qq_def)
23.73 with posbb
23.74 show "\<forall> l. norm_unsigned (nat_to_bv_helper (number_of (bin BIT b)) l) = norm_unsigned (fast_nat_to_bv_helper (bin BIT b) l)"
23.75 - apply (subst pos_number_of,simp)
23.76 + apply (subst pos_number_of)
23.77 apply safe
23.78 apply (fold qq_def)
23.79 apply (cases "qq = 0")
23.80 @@ -2938,6 +2938,8 @@
23.81 declare fast_nat_to_bv_Bit [simp del]
23.82 declare fast_nat_to_bv_Bit0 [simp]
23.83 declare fast_nat_to_bv_Bit1 [simp]
23.84 +****)
23.85 +
23.86
23.87 consts
23.88 fast_bv_to_nat_helper :: "[bit list, bin] => bin"
23.89 @@ -2952,13 +2954,13 @@
23.90 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)"
23.91 by simp
23.92
23.93 -lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs bin.Pls)"
23.94 +lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
23.95 proof (simp add: bv_to_nat_def)
23.96 have "\<forall> bin. (foldl (%bn b. bn BIT (b = \<one>)) bin bs) = (fast_bv_to_nat_helper bs bin)"
23.97 apply (induct bs,simp)
23.98 apply (case_tac a,simp_all)
23.99 done
23.100 - thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bs) == number_of (fast_bv_to_nat_helper bs bin.Pls)::int"
23.101 + thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bs) == number_of (fast_bv_to_nat_helper bs Numeral.Pls)::int"
23.102 by simp
23.103 qed
23.104
23.105 @@ -2988,12 +2990,4 @@
23.106 lemma [code]: "bv_to_nat bs = list_rec (0::int) (\<lambda>b bs n. bitval b * 2 ^ length bs + n) bs"
23.107 by (induct bs,simp_all add: bv_to_nat_helper)
23.108
23.109 -text {* The following can be added for speedup, but depends on the
23.110 -exact definition of division and modulo of the ML compiler for soundness. *}
23.111 -
23.112 -(*
23.113 -consts_code "op div" ("'('(_') div '(_')')")
23.114 -consts_code "op mod" ("'('(_') mod '(_')')")
23.115 -*)
23.116 -
23.117 end
24.1 --- a/src/HOL/Library/word_setup.ML Wed Jun 30 14:04:58 2004 +0200
24.2 +++ b/src/HOL/Library/word_setup.ML Thu Jul 01 12:29:53 2004 +0200
24.3 @@ -1,6 +1,8 @@
24.4 (* Title: HOL/Library/word_setup.ML
24.5 ID: $Id$
24.6 Author: Sebastian Skalberg (TU Muenchen)
24.7 +
24.8 +comments containing lcp are the removal of fast_bv_of_nat.
24.9 *)
24.10
24.11 local
24.12 @@ -10,9 +12,9 @@
24.13 fun is_const_bit (Const("Word.bit.Zero",_)) = true
24.14 | is_const_bit (Const("Word.bit.One",_)) = true
24.15 | is_const_bit _ = false
24.16 - fun num_is_usable (Const("Numeral.bin.Pls",_)) = true
24.17 - | num_is_usable (Const("Numeral.bin.Min",_)) = false
24.18 - | num_is_usable (Const("Numeral.bin.Bit",_) $ w $ b) =
24.19 + fun num_is_usable (Const("Numeral.Pls",_)) = true
24.20 + | num_is_usable (Const("Numeral.Min",_)) = false
24.21 + | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
24.22 num_is_usable w andalso is_const_bool b
24.23 | num_is_usable _ = false
24.24 fun vec_is_usable (Const("List.list.Nil",_)) = true
24.25 @@ -21,22 +23,22 @@
24.26 | vec_is_usable _ = false
24.27 fun add_word thy =
24.28 let
24.29 - val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"
24.30 + (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
24.31 val fast2_th = PureThy.get_thm thy "Word.fast_bv_to_nat_def"
24.32 - fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
24.33 + (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
24.34 if num_is_usable t
24.35 then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
24.36 else None
24.37 - | f _ _ _ = None
24.38 + | f _ _ _ = None **)
24.39 fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
24.40 if vec_is_usable t
24.41 then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
24.42 else None
24.43 | g _ _ _ = None
24.44 - val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f
24.45 + (*lcp** val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
24.46 val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
24.47 in
24.48 - Simplifier.change_simpset_of (op addsimprocs) [simproc1,simproc2] thy
24.49 + Simplifier.change_simpset_of (op addsimprocs) [(*lcp*simproc1,**)simproc2] thy
24.50 end
24.51 in
24.52 val setup_word = [add_word]
25.1 --- a/src/HOL/Numeral.thy Wed Jun 30 14:04:58 2004 +0200
25.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
25.3 @@ -1,195 +0,0 @@
25.4 -(* Title: HOL/Numeral.thy
25.5 - ID: $Id$
25.6 - Author: Larry Paulson and Markus Wenzel
25.7 -
25.8 -Generic numerals represented as twos-complement bit strings.
25.9 -*)
25.10 -
25.11 -theory Numeral = Datatype
25.12 -files "Tools/numeral_syntax.ML":
25.13 -
25.14 -text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
25.15 - Only qualified access bin.Pls and bin.Min is allowed.
25.16 - We do not hide Bit because we need the BIT infix syntax.*}
25.17 -
25.18 -text{*A number can have multiple representations, namely leading Falses with
25.19 -sign @{term Pls} and leading Trues with sign @{term Min}.
25.20 -See @{text "ZF/Integ/twos-compl.ML"}, function @{text int_of_binary},
25.21 -for the numerical interpretation.
25.22 -
25.23 -The representation expects that @{text "(m mod 2)"} is 0 or 1,
25.24 -even if m is negative;
25.25 -For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
25.26 -@{text "-5 = (-3)*2 + 1"}.
25.27 -*}
25.28 -
25.29 -datatype
25.30 - bin = Pls --{*Plus: Stands for an infinite string of leading Falses*}
25.31 - | Min --{*Minus: Stands for an infinite string of leading Trues*}
25.32 - | Bit bin bool (infixl "BIT" 90)
25.33 -
25.34 -axclass
25.35 - number < type -- {* for numeric types: nat, int, real, \dots *}
25.36 -
25.37 -consts
25.38 - number_of :: "bin => 'a::number"
25.39 -
25.40 -syntax
25.41 - "_Numeral" :: "num_const => 'a" ("_")
25.42 - Numeral0 :: 'a
25.43 - Numeral1 :: 'a
25.44 -
25.45 -translations
25.46 - "Numeral0" == "number_of bin.Pls"
25.47 - "Numeral1" == "number_of (bin.Pls BIT True)"
25.48 -
25.49 -
25.50 -setup NumeralSyntax.setup
25.51 -
25.52 -syntax (xsymbols)
25.53 - "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
25.54 -syntax (HTML output)
25.55 - "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
25.56 -syntax (output)
25.57 - "_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
25.58 -translations
25.59 - "x\<twosuperior>" == "x^2"
25.60 - "x\<twosuperior>" <= "x^(2::nat)"
25.61 -
25.62 -
25.63 -lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
25.64 - -- {* Unfold all @{text let}s involving constants *}
25.65 - by (simp add: Let_def)
25.66 -
25.67 -lemma Let_0 [simp]: "Let 0 f == f 0"
25.68 - by (simp add: Let_def)
25.69 -
25.70 -lemma Let_1 [simp]: "Let 1 f == f 1"
25.71 - by (simp add: Let_def)
25.72 -
25.73 -
25.74 -consts
25.75 - NCons :: "[bin,bool]=>bin"
25.76 - bin_succ :: "bin=>bin"
25.77 - bin_pred :: "bin=>bin"
25.78 - bin_minus :: "bin=>bin"
25.79 - bin_add :: "[bin,bin]=>bin"
25.80 - bin_mult :: "[bin,bin]=>bin"
25.81 -
25.82 -text{*@{term NCons} inserts a bit, suppressing leading 0s and 1s*}
25.83 -primrec
25.84 - NCons_Pls: "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
25.85 - NCons_Min: "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
25.86 - NCons_BIT: "NCons (w BIT x) b = (w BIT x) BIT b"
25.87 -
25.88 -
25.89 -primrec
25.90 - bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True"
25.91 - bin_succ_Min: "bin_succ bin.Min = bin.Pls"
25.92 - bin_succ_BIT: "bin_succ(w BIT x) =
25.93 - (if x then bin_succ w BIT False
25.94 - else NCons w True)"
25.95 -
25.96 -primrec
25.97 - bin_pred_Pls: "bin_pred bin.Pls = bin.Min"
25.98 - bin_pred_Min: "bin_pred bin.Min = bin.Min BIT False"
25.99 - bin_pred_BIT: "bin_pred(w BIT x) =
25.100 - (if x then NCons w False
25.101 - else (bin_pred w) BIT True)"
25.102 -
25.103 -primrec
25.104 - bin_minus_Pls: "bin_minus bin.Pls = bin.Pls"
25.105 - bin_minus_Min: "bin_minus bin.Min = bin.Pls BIT True"
25.106 - bin_minus_BIT: "bin_minus(w BIT x) =
25.107 - (if x then bin_pred (NCons (bin_minus w) False)
25.108 - else bin_minus w BIT False)"
25.109 -
25.110 -primrec
25.111 - bin_add_Pls: "bin_add bin.Pls w = w"
25.112 - bin_add_Min: "bin_add bin.Min w = bin_pred w"
25.113 - bin_add_BIT:
25.114 - "bin_add (v BIT x) w =
25.115 - (case w of bin.Pls => v BIT x
25.116 - | bin.Min => bin_pred (v BIT x)
25.117 - | (w BIT y) =>
25.118 - NCons (bin_add v (if (x & y) then bin_succ w else w))
25.119 - (x~=y))"
25.120 -
25.121 -primrec
25.122 - bin_mult_Pls: "bin_mult bin.Pls w = bin.Pls"
25.123 - bin_mult_Min: "bin_mult bin.Min w = bin_minus w"
25.124 - bin_mult_BIT: "bin_mult (v BIT x) w =
25.125 - (if x then (bin_add (NCons (bin_mult v w) False) w)
25.126 - else (NCons (bin_mult v w) False))"
25.127 -
25.128 -
25.129 -subsection{*Extra rules for @{term bin_succ}, @{term bin_pred},
25.130 - @{term bin_add} and @{term bin_mult}*}
25.131 -
25.132 -lemma NCons_Pls_0: "NCons bin.Pls False = bin.Pls"
25.133 -by simp
25.134 -
25.135 -lemma NCons_Pls_1: "NCons bin.Pls True = bin.Pls BIT True"
25.136 -by simp
25.137 -
25.138 -lemma NCons_Min_0: "NCons bin.Min False = bin.Min BIT False"
25.139 -by simp
25.140 -
25.141 -lemma NCons_Min_1: "NCons bin.Min True = bin.Min"
25.142 -by simp
25.143 -
25.144 -lemma bin_succ_1: "bin_succ(w BIT True) = (bin_succ w) BIT False"
25.145 -by simp
25.146 -
25.147 -lemma bin_succ_0: "bin_succ(w BIT False) = NCons w True"
25.148 -by simp
25.149 -
25.150 -lemma bin_pred_1: "bin_pred(w BIT True) = NCons w False"
25.151 -by simp
25.152 -
25.153 -lemma bin_pred_0: "bin_pred(w BIT False) = (bin_pred w) BIT True"
25.154 -by simp
25.155 -
25.156 -lemma bin_minus_1: "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
25.157 -by simp
25.158 -
25.159 -lemma bin_minus_0: "bin_minus(w BIT False) = (bin_minus w) BIT False"
25.160 -by simp
25.161 -
25.162 -
25.163 -subsection{*Binary Addition and Multiplication:
25.164 - @{term bin_add} and @{term bin_mult}*}
25.165 -
25.166 -lemma bin_add_BIT_11:
25.167 - "bin_add (v BIT True) (w BIT True) =
25.168 - NCons (bin_add v (bin_succ w)) False"
25.169 -by simp
25.170 -
25.171 -lemma bin_add_BIT_10:
25.172 - "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
25.173 -by simp
25.174 -
25.175 -lemma bin_add_BIT_0:
25.176 - "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
25.177 -by auto
25.178 -
25.179 -lemma bin_add_Pls_right: "bin_add w bin.Pls = w"
25.180 -by (induct_tac "w", auto)
25.181 -
25.182 -lemma bin_add_Min_right: "bin_add w bin.Min = bin_pred w"
25.183 -by (induct_tac "w", auto)
25.184 -
25.185 -lemma bin_add_BIT_BIT:
25.186 - "bin_add (v BIT x) (w BIT y) =
25.187 - NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
25.188 -by simp
25.189 -
25.190 -lemma bin_mult_1:
25.191 - "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
25.192 -by simp
25.193 -
25.194 -lemma bin_mult_0: "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
25.195 -by simp
25.196 -
25.197 -
25.198 -end
26.1 --- a/src/HOL/Presburger.thy Wed Jun 30 14:04:58 2004 +0200
26.2 +++ b/src/HOL/Presburger.thy Thu Jul 01 12:29:53 2004 +0200
26.3 @@ -969,7 +969,7 @@
26.4 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
26.5 by simp
26.6
26.7 -theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
26.8 +theorem number_of2: "(0::int) <= Numeral0" by simp
26.9
26.10 theorem Suc_plus1: "Suc n = n + 1" by simp
26.11
27.1 --- a/src/HOL/Real/PReal.thy Wed Jun 30 14:04:58 2004 +0200
27.2 +++ b/src/HOL/Real/PReal.thy Thu Jul 01 12:29:53 2004 +0200
27.3 @@ -705,7 +705,7 @@
27.4 from preal_nonempty [OF A]
27.5 show ?case by force
27.6 case (Suc k)
27.7 - from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" ..
27.8 + from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
27.9 hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
27.10 thus ?case by (force simp add: left_distrib add_ac prems)
27.11 qed
28.1 --- a/src/HOL/Real/Rational.thy Wed Jun 30 14:04:58 2004 +0200
28.2 +++ b/src/HOL/Real/Rational.thy Thu Jul 01 12:29:53 2004 +0200
28.3 @@ -674,25 +674,12 @@
28.4
28.5 instance rat :: number ..
28.6
28.7 -primrec -- {* the type constraint is essential! *}
28.8 - number_of_Pls: "number_of bin.Pls = 0"
28.9 - number_of_Min: "number_of bin.Min = - (1::rat)"
28.10 - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
28.11 - (number_of w) + (number_of w)"
28.12 -
28.13 -declare number_of_Pls [simp del]
28.14 - number_of_Min [simp del]
28.15 - number_of_BIT [simp del]
28.16 +defs (overloaded)
28.17 + rat_number_of_def: "(number_of w :: rat) == of_int (Rep_Bin w)"
28.18 + --{*the type constraint is essential!*}
28.19
28.20 instance rat :: number_ring
28.21 -proof
28.22 - show "Numeral0 = (0::rat)" by (rule number_of_Pls)
28.23 - show "-1 = - (1::rat)" by (rule number_of_Min)
28.24 - fix w :: bin and x :: bool
28.25 - show "(number_of (w BIT x) :: rat) =
28.26 - (if x then 1 else 0) + number_of w + number_of w"
28.27 - by (rule number_of_BIT)
28.28 -qed
28.29 +by (intro_classes, simp add: rat_number_of_def)
28.30
28.31 declare diff_rat_def [symmetric]
28.32
29.1 --- a/src/HOL/Real/RealDef.thy Wed Jun 30 14:04:58 2004 +0200
29.2 +++ b/src/HOL/Real/RealDef.thy Thu Jul 01 12:29:53 2004 +0200
29.3 @@ -732,25 +732,12 @@
29.4
29.5 instance real :: number ..
29.6
29.7 -primrec (*the type constraint is essential!*)
29.8 - number_of_Pls: "number_of bin.Pls = 0"
29.9 - number_of_Min: "number_of bin.Min = - (1::real)"
29.10 - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
29.11 - (number_of w) + (number_of w)"
29.12 -
29.13 -declare number_of_Pls [simp del]
29.14 - number_of_Min [simp del]
29.15 - number_of_BIT [simp del]
29.16 +defs (overloaded)
29.17 + real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
29.18 + --{*the type constraint is essential!*}
29.19
29.20 instance real :: number_ring
29.21 -proof
29.22 - show "Numeral0 = (0::real)" by (rule number_of_Pls)
29.23 - show "-1 = - (1::real)" by (rule number_of_Min)
29.24 - fix w :: bin and x :: bool
29.25 - show "(number_of (w BIT x) :: real) =
29.26 - (if x then 1 else 0) + number_of w + number_of w"
29.27 - by (rule number_of_BIT)
29.28 -qed
29.29 +by (intro_classes, simp add: real_number_of_def)
29.30
29.31
29.32 text{*Collapse applications of @{term real} to @{term number_of}*}
30.1 --- a/src/HOL/Tools/Presburger/presburger.ML Wed Jun 30 14:04:58 2004 +0200
30.2 +++ b/src/HOL/Tools/Presburger/presburger.ML Thu Jul 01 12:29:53 2004 +0200
30.3 @@ -120,9 +120,9 @@
30.4 ("HOL.max", nT --> nT --> nT),
30.5 ("HOL.min", nT --> nT --> nT),
30.6
30.7 - ("Numeral.bin.Bit", binT --> bT --> binT),
30.8 - ("Numeral.bin.Pls", binT),
30.9 - ("Numeral.bin.Min", binT),
30.10 + ("Numeral.Bit", binT --> bT --> binT),
30.11 + ("Numeral.Pls", binT),
30.12 + ("Numeral.Min", binT),
30.13 ("Numeral.number_of", binT --> iT),
30.14 ("Numeral.number_of", binT --> nT),
30.15 ("0", nT),
31.1 --- a/src/HOL/Tools/numeral_syntax.ML Wed Jun 30 14:04:58 2004 +0200
31.2 +++ b/src/HOL/Tools/numeral_syntax.ML Thu Jul 01 12:29:53 2004 +0200
31.3 @@ -28,8 +28,8 @@
31.4 | prefix_len pred (x :: xs) =
31.5 if pred x then 1 + prefix_len pred xs else 0;
31.6
31.7 -fun bin_of (Const ("bin.Pls", _)) = []
31.8 - | bin_of (Const ("bin.Min", _)) = [~1]
31.9 +fun bin_of (Const ("Numeral.Pls", _)) = []
31.10 + | bin_of (Const ("Numeral.Min", _)) = [~1]
31.11 | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
31.12 | bin_of _ = raise Match;
31.13
31.14 @@ -70,7 +70,7 @@
31.15 (* theory setup *)
31.16
31.17 val setup =
31.18 - [Theory.hide_consts false ["Numeral.bin.Pls", "Numeral.bin.Min"],
31.19 + [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
31.20 Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
31.21 Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
31.22
32.1 --- a/src/HOL/ex/BinEx.thy Wed Jun 30 14:04:58 2004 +0200
32.2 +++ b/src/HOL/ex/BinEx.thy Thu Jul 01 12:29:53 2004 +0200
32.3 @@ -387,115 +387,7 @@
32.4 by simp
32.5
32.6
32.7 -subsection {* Normal form of bit strings *}
32.8 -
32.9 -text {*
32.10 - Definition of normal form for proving that binary arithmetic on
32.11 - normalized operands yields normalized results. Normal means no
32.12 - leading 0s on positive numbers and no leading 1s on negatives.
32.13 -*}
32.14 -
32.15 -consts normal :: "bin set"
32.16 -inductive normal
32.17 - intros
32.18 - Pls [simp]: "bin.Pls: normal"
32.19 - Min [simp]: "bin.Min: normal"
32.20 - BIT_F [simp]: "w: normal ==> w \<noteq> bin.Pls ==> w BIT False : normal"
32.21 - BIT_T [simp]: "w: normal ==> w \<noteq> bin.Min ==> w BIT True : normal"
32.22 -
32.23 -text {*
32.24 - \medskip Binary arithmetic on normalized operands yields normalized
32.25 - results.
32.26 -*}
32.27 -
32.28 -lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal"
32.29 - apply (case_tac c)
32.30 - apply auto
32.31 - done
32.32 -
32.33 -lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal"
32.34 - apply (erule normal.cases)
32.35 - apply auto
32.36 - done
32.37 -
32.38 -lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal"
32.39 - apply (induct w)
32.40 - apply (auto simp add: NCons_Pls NCons_Min)
32.41 - done
32.42 -
32.43 -lemma NCons_True: "NCons w True \<noteq> bin.Pls"
32.44 - apply (induct w)
32.45 - apply auto
32.46 - done
32.47 -
32.48 -lemma NCons_False: "NCons w False \<noteq> bin.Min"
32.49 - apply (induct w)
32.50 - apply auto
32.51 - done
32.52 -
32.53 -lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> normal"
32.54 - apply (erule normal.induct)
32.55 - apply (case_tac [4] w)
32.56 - apply (auto simp add: NCons_True bin_succ_BIT)
32.57 - done
32.58 -
32.59 -lemma bin_pred_normal [simp]: "w \<in> normal ==> bin_pred w \<in> normal"
32.60 - apply (erule normal.induct)
32.61 - apply (case_tac [3] w)
32.62 - apply (auto simp add: NCons_False bin_pred_BIT)
32.63 - done
32.64 -
32.65 -lemma bin_add_normal [rule_format]:
32.66 - "w \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> normal)"
32.67 - apply (induct w)
32.68 - apply simp
32.69 - apply simp
32.70 - apply (rule impI)
32.71 - apply (rule allI)
32.72 - apply (induct_tac z)
32.73 - apply (simp_all add: bin_add_BIT)
32.74 - apply (safe dest!: normal_BIT_D)
32.75 - apply simp_all
32.76 - done
32.77 -
32.78 -lemma normal_Pls_eq_0: "w \<in> normal ==> (w = bin.Pls) = (number_of w = (0::int))"
32.79 - apply (erule normal.induct)
32.80 - apply auto
32.81 - done
32.82 -
32.83 -lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"
32.84 - apply (erule normal.induct)
32.85 - apply (simp_all add: bin_minus_BIT)
32.86 - apply (rule normal.intros)
32.87 - apply assumption
32.88 - apply (simp add: normal_Pls_eq_0)
32.89 - apply (simp only: number_of_minus zminus_0 iszero_def
32.90 - minus_equation_iff [of _ "0"])
32.91 - done
32.92 -
32.93 -(*The previous command should have finished the proof but the lin-arith
32.94 -procedure at the end of simplificatioon fails.
32.95 -Problem: lin-arith correctly derives the contradictory thm
32.96 -"number_of w + 1 + - 0 \<le> 0 + number_of w" [..]
32.97 -which its local simplification setup should turn into False.
32.98 -But on the way we get
32.99 -
32.100 -Procedure "int_add_eval_numerals" produced rewrite rule:
32.101 -number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (bin.Pls BIT True))
32.102 -
32.103 -and eventually we arrive not at false but at
32.104 -
32.105 -"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (bin.Pls BIT True)))))"
32.106 -
32.107 -The simplification with eq_commute should now be obsolete.
32.108 -*)
32.109 -
32.110 -lemma bin_mult_normal [rule_format]:
32.111 - "w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"
32.112 - apply (erule normal.induct)
32.113 - apply (simp_all add: bin_minus_normal bin_mult_BIT)
32.114 - apply (safe dest!: normal_BIT_D)
32.115 - apply (simp add: bin_add_normal)
32.116 - done
32.117 +text{*The proofs about arithmetic yielding normal forms have been deleted:
32.118 + they are irrelevant with the new treatment of numerals.*}
32.119
32.120 end
33.1 --- a/src/HOL/hologic.ML Wed Jun 30 14:04:58 2004 +0200
33.2 +++ b/src/HOL/hologic.ML Thu Jul 01 12:29:53 2004 +0200
33.3 @@ -282,9 +282,9 @@
33.4
33.5 val binT = Type ("Numeral.bin", []);
33.6
33.7 -val pls_const = Const ("Numeral.bin.Pls", binT)
33.8 -and min_const = Const ("Numeral.bin.Min", binT)
33.9 -and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
33.10 +val pls_const = Const ("Numeral.Pls", binT)
33.11 +and min_const = Const ("Numeral.Min", binT)
33.12 +and bit_const = Const ("Numeral.Bit", [binT, boolT] ---> binT);
33.13
33.14 fun number_of_const T = Const ("Numeral.number_of", binT --> T);
33.15
33.16 @@ -296,9 +296,9 @@
33.17 | dest_bit (Const ("True", _)) = 1
33.18 | dest_bit t = raise TERM("dest_bit", [t]);
33.19
33.20 -fun bin_of (Const ("Numeral.bin.Pls", _)) = []
33.21 - | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
33.22 - | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
33.23 +fun bin_of (Const ("Numeral.Pls", _)) = []
33.24 + | bin_of (Const ("Numeral.Min", _)) = [~1]
33.25 + | bin_of (Const ("Numeral.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
33.26 | bin_of t = raise TERM("bin_of", [t]);
33.27
33.28 val dest_binum = int_of o bin_of;