--- a/src/HOL/Complex/CLim.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/CLim.thy Thu Jul 01 12:29:53 2004 +0200
@@ -666,8 +666,8 @@
apply (subgoal_tac "xa + - (hcomplex_of_complex x) \<noteq> 0")
prefer 2 apply (simp add: compare_rls)
apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec)
- prefer 2 apply (simp add: hcomplex_add_assoc [symmetric])
-apply (auto simp add: mem_cinfmal_iff [symmetric] hcomplex_add_commute)
+ prefer 2 apply (simp add: add_assoc [symmetric])
+apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute)
apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1)
apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
simp add: mult_assoc)
@@ -740,7 +740,7 @@
CInfinitesimal_add CInfinitesimal_mult
CInfinitesimal_hcomplex_of_complex_mult
CInfinitesimal_hcomplex_of_complex_mult2
- simp add: hcomplex_add_assoc [symmetric])
+ simp add: add_assoc [symmetric])
done
lemma CDERIV_mult:
@@ -899,7 +899,7 @@
"CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
apply (induct_tac "n")
apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult])
-apply (auto simp add: complex_of_real_add [symmetric] left_distrib real_of_nat_Suc)
+apply (auto simp add: left_distrib real_of_nat_Suc)
apply (case_tac "n")
apply (auto simp add: mult_ac add_commute)
done
@@ -930,7 +930,8 @@
apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add
inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
add_ac mult_ac
- del: inverse_minus_eq inverse_mult_distrib minus_mult_right [symmetric] minus_mult_left [symmetric])
+ del: inverse_minus_eq inverse_mult_distrib
+ minus_mult_right [symmetric] minus_mult_left [symmetric])
apply (simp only: mult_assoc [symmetric] right_distrib)
apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans)
apply (rule inverse_add_CInfinitesimal_capprox2)
@@ -952,7 +953,8 @@
"[| CDERIV f x :> d; f(x) \<noteq> 0 |]
==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
apply (rule mult_commute [THEN subst])
-apply (simp (no_asm_simp) add: minus_mult_left power_inverse del: complexpow_Suc minus_mult_left [symmetric])
+apply (simp add: minus_mult_left power_inverse
+ del: complexpow_Suc minus_mult_left [symmetric])
apply (fold o_def)
apply (blast intro!: CDERIV_chain CDERIV_inverse)
done
--- a/src/HOL/Complex/CSeries.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/CSeries.thy Thu Jul 01 12:29:53 2004 +0200
@@ -72,7 +72,7 @@
lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
apply (induct_tac "n")
-apply (auto simp add: left_distrib complex_of_real_add [symmetric] real_of_nat_Suc)
+apply (auto simp add: left_distrib real_of_nat_Suc)
done
lemma sumc_add_mult_const:
@@ -98,16 +98,16 @@
lemma sumc_interval_const [rule_format (no_asm)]:
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
- --> sumc m na f = (complex_of_real(real (na - m)) * r)"
+ --> sumc m na f = (complex_of_real(real (na - m)) * r)"
apply (induct_tac "na")
-apply (auto simp add: Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric] left_distrib)
+apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
done
lemma sumc_interval_const2 [rule_format (no_asm)]:
"(\<forall>n. m \<le> n --> f n = r) & m \<le> na
--> sumc m na f = (complex_of_real(real (na - m)) * r)"
apply (induct_tac "na")
-apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric])
+apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
done
(***
--- a/src/HOL/Complex/Complex.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/Complex.thy Thu Jul 01 12:29:53 2004 +0200
@@ -291,35 +291,33 @@
"(complex_of_real x = complex_of_real y) = (x = y)"
by (simp add: complex_of_real_def)
-lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"
+lemma complex_of_real_minus [simp]: "complex_of_real(-x) = - complex_of_real x"
by (simp add: complex_of_real_def complex_minus)
-lemma complex_of_real_inverse:
+lemma complex_of_real_inverse [simp]:
"complex_of_real(inverse x) = inverse(complex_of_real x)"
apply (case_tac "x=0", simp)
-apply (simp add: complex_inverse complex_of_real_def real_divide_def
- inverse_mult_distrib power2_eq_square)
+apply (simp add: complex_of_real_def divide_inverse power2_eq_square)
done
-lemma complex_of_real_add:
- "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
+lemma complex_of_real_add [simp]:
+ "complex_of_real (x + y) = complex_of_real x + complex_of_real y"
by (simp add: complex_add complex_of_real_def)
-lemma complex_of_real_diff:
- "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
-by (simp add: complex_of_real_minus [symmetric] complex_diff_def
- complex_of_real_add)
+lemma complex_of_real_diff [simp]:
+ "complex_of_real (x - y) = complex_of_real x - complex_of_real y"
+by (simp add: complex_of_real_minus diff_minus)
-lemma complex_of_real_mult:
- "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
+lemma complex_of_real_mult [simp]:
+ "complex_of_real (x * y) = complex_of_real x * complex_of_real y"
by (simp add: complex_mult complex_of_real_def)
-lemma complex_of_real_divide:
- "complex_of_real x / complex_of_real y = complex_of_real(x/y)"
+lemma complex_of_real_divide [simp]:
+ "complex_of_real(x/y) = complex_of_real x / complex_of_real y"
apply (simp add: complex_divide_def)
apply (case_tac "y=0", simp)
-apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse
- real_divide_def)
+apply (simp add: complex_of_real_mult complex_of_real_inverse
+ divide_inverse)
done
lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
@@ -407,7 +405,7 @@
by (induct w, induct z, simp add: complex_cnj complex_add)
lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
-by (simp add: complex_diff_def complex_cnj_add complex_cnj_minus)
+by (simp add: diff_minus complex_cnj_add complex_cnj_minus)
lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
by (induct w, induct z, simp add: complex_cnj complex_mult)
@@ -423,7 +421,7 @@
lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
apply (induct z)
-apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def
+apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus
complex_minus i_def complex_mult)
done
@@ -561,7 +559,7 @@
done
lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
-by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse)
+by (simp add: complex_divide_def divide_inverse complex_mod_mult complex_mod_inverse)
subsection{*Exponentiation*}
@@ -639,24 +637,33 @@
lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
by (simp add: i_def)
+
+
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
-apply (induct z)
-apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
-apply (simp add: complex_of_real_def complex_mult real_divide_def)
-done
+proof (induct z)
+ case (Complex x y)
+ have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
+ by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
+ thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)"
+ by (simp add: sgn_def complex_of_real_def divide_inverse)
+qed
+
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
-apply (induct z)
-apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
-apply (simp add: complex_of_real_def complex_mult real_divide_def)
-done
+proof (induct z)
+ case (Complex x y)
+ have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
+ by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
+ thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)"
+ by (simp add: sgn_def complex_of_real_def divide_inverse)
+qed
lemma complex_inverse_complex_split:
"inverse(complex_of_real x + ii * complex_of_real y) =
complex_of_real(x/(x ^ 2 + y ^ 2)) -
ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
by (simp add: complex_of_real_def i_def complex_mult complex_add
- complex_diff_def complex_minus complex_inverse real_divide_def)
+ diff_minus complex_minus complex_inverse divide_inverse)
(*----------------------------------------------------------------------------*)
(* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
@@ -738,7 +745,8 @@
by (simp add: rcis_def)
lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib)
+by (simp add: rcis_def cis_def cos_add sin_add right_distrib right_diff_distrib
+ complex_of_real_def)
lemma cis_mult: "cis a * cis b = cis (a + b)"
by (simp add: cis_rcis_eq rcis_mult)
@@ -774,7 +782,7 @@
lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus
- complex_diff_def)
+ diff_minus)
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
by (simp add: divide_inverse rcis_def complex_of_real_inverse)
@@ -818,33 +826,31 @@
instance complex :: number ..
-primrec (*the type constraint is essential!*)
- number_of_Pls: "number_of bin.Pls = 0"
- number_of_Min: "number_of bin.Min = - (1::complex)"
- number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
- number_of_Min [simp del]
- number_of_BIT [simp del]
+defs (overloaded)
+ complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
+ --{*the type constraint is essential!*}
instance complex :: number_ring
-proof
- show "Numeral0 = (0::complex)" by (rule number_of_Pls)
- show "-1 = - (1::complex)" by (rule number_of_Min)
- fix w :: bin and x :: bool
- show "(number_of (w BIT x) :: complex) =
- (if x then 1 else 0) + number_of w + number_of w"
- by (rule number_of_BIT)
+by (intro_classes, simp add: complex_number_of_def)
+
+
+lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n"
+by (induct n, simp_all)
+
+lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z"
+proof (cases z)
+ case (1 n)
+ thus ?thesis by simp
+next
+ case (2 n)
+ thus ?thesis
+ by (simp only: of_int_minus complex_of_real_minus, simp)
qed
text{*Collapse applications of @{term complex_of_real} to @{term number_of}*}
lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
-apply (induct w)
-apply (simp_all only: number_of complex_of_real_add [symmetric]
- complex_of_real_minus, simp_all)
-done
+by (simp add: complex_number_of_def real_number_of_def)
text{*This theorem is necessary because theorems such as
@{text iszero_number_of_0} only hold for ordered rings. They cannot
@@ -855,50 +861,6 @@
by (simp only: complex_of_real_zero_iff complex_number_of [symmetric]
iszero_def)
-
-(*These allow simplification of expressions involving mixed numbers.
- Convert???
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + ii * number_of ya =
- number_of xb) =
- (((number_of xa :: complex) = number_of xb) &
- ((number_of ya :: complex) = 0))"
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2,
- complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff2";
-Addsimps [complex_number_of_eq_cancel_iff2];
-
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + number_of ya * ii = \
-\ number_of xb) = \
-\ (((number_of xa :: complex) = number_of xb) & \
-\ ((number_of ya :: complex) = 0))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2a,
- complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff2a";
-Addsimps [complex_number_of_eq_cancel_iff2a];
-
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + ii * number_of ya = \
-\ ii * number_of yb) = \
-\ (((number_of xa :: complex) = 0) & \
-\ ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3,
- complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff3";
-Addsimps [complex_number_of_eq_cancel_iff3];
-
-Goalw [complex_number_of_def]
- "((number_of xa :: complex) + number_of ya * ii= \
-\ ii * number_of yb) = \
-\ (((number_of xa :: complex) = 0) & \
-\ ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3a,
- complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff3a";
-Addsimps [complex_number_of_eq_cancel_iff3a];
-*)
-
lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
apply (subst complex_number_of [symmetric])
apply (rule complex_cnj_complex_of_real)
@@ -957,7 +919,6 @@
val complex_zero_def = thm"complex_zero_def";
val complex_one_def = thm"complex_one_def";
val complex_minus_def = thm"complex_minus_def";
-val complex_diff_def = thm"complex_diff_def";
val complex_divide_def = thm"complex_divide_def";
val complex_mult_def = thm"complex_mult_def";
val complex_add_def = thm"complex_add_def";
--- a/src/HOL/Complex/NSCA.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/NSCA.thy Thu Jul 01 12:29:53 2004 +0200
@@ -508,7 +508,7 @@
lemma capprox_SComplex_mult_cancel_zero:
"[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0"
apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
-apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
+apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
done
lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
@@ -524,7 +524,7 @@
lemma capprox_SComplex_mult_cancel:
"[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z"
apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
-apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
+apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
done
lemma capprox_SComplex_mult_cancel_iff1 [simp]:
@@ -618,7 +618,7 @@
lemma CInfinitesimal_ratio:
"[| y \<noteq> 0; y \<in> CInfinitesimal; x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
apply (drule CInfinitesimal_CFinite_mult2, assumption)
-apply (simp add: divide_inverse hcomplex_mult_assoc)
+apply (simp add: divide_inverse mult_assoc)
done
lemma SComplex_capprox_iff:
@@ -901,10 +901,11 @@
apply (drule CFinite_inverse2)+
apply (drule capprox_mult2, assumption, auto)
apply (drule_tac c = "inverse x" in capprox_mult1, assumption)
-apply (auto intro: capprox_sym simp add: hcomplex_mult_assoc)
+apply (auto intro: capprox_sym simp add: mult_assoc)
done
-lemmas hcomplex_of_complex_capprox_inverse = hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
+lemmas hcomplex_of_complex_capprox_inverse =
+ hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
lemma inverse_add_CInfinitesimal_capprox:
"[| x \<in> CFinite - CInfinitesimal;
@@ -935,7 +936,7 @@
apply safe
apply (frule CFinite_inverse, assumption)
apply (drule not_CInfinitesimal_not_zero)
-apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
+apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
done
lemma capprox_CFinite_mult_cancel_iff1:
--- a/src/HOL/Complex/NSComplex.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy Thu Jul 01 12:29:53 2004 +0200
@@ -475,51 +475,48 @@
apply (simp add: hcomplex_of_hypreal)
done
-lemma hcomplex_of_hypreal_minus:
- "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-apply (cases x)
-apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
-done
-
-lemma hcomplex_of_hypreal_inverse:
- "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-apply (cases x)
-apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
-done
-
-lemma hcomplex_of_hypreal_add:
- "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
- hcomplex_of_hypreal (x + y)"
-apply (cases x, cases y)
-apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
-done
-
-lemma hcomplex_of_hypreal_diff:
- "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
- hcomplex_of_hypreal (x - y)"
-by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
-
-lemma hcomplex_of_hypreal_mult:
- "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
- hcomplex_of_hypreal (x * y)"
-apply (cases x, cases y)
-apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
-done
-
-lemma hcomplex_of_hypreal_divide:
- "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
-apply (simp add: hcomplex_divide_def)
-apply (case_tac "y=0", simp)
-apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
-apply (simp add: hypreal_divide_def)
-done
-
lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num)
lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
+lemma hcomplex_of_hypreal_minus [simp]:
+ "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
+apply (cases x)
+apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus)
+done
+
+lemma hcomplex_of_hypreal_inverse [simp]:
+ "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
+apply (cases x)
+apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse)
+done
+
+lemma hcomplex_of_hypreal_add [simp]:
+ "hcomplex_of_hypreal (x + y) = hcomplex_of_hypreal x + hcomplex_of_hypreal y"
+apply (cases x, cases y)
+apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add)
+done
+
+lemma hcomplex_of_hypreal_diff [simp]:
+ "hcomplex_of_hypreal (x - y) =
+ hcomplex_of_hypreal x - hcomplex_of_hypreal y "
+by (simp add: hcomplex_diff_def hypreal_diff_def)
+
+lemma hcomplex_of_hypreal_mult [simp]:
+ "hcomplex_of_hypreal (x * y) = hcomplex_of_hypreal x * hcomplex_of_hypreal y"
+apply (cases x, cases y)
+apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult)
+done
+
+lemma hcomplex_of_hypreal_divide [simp]:
+ "hcomplex_of_hypreal(x/y) = hcomplex_of_hypreal x / hcomplex_of_hypreal y"
+apply (simp add: hcomplex_divide_def)
+apply (case_tac "y=0", simp)
+apply (simp add: hypreal_divide_def)
+done
+
lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
apply (cases z)
apply (auto simp add: hcomplex_of_hypreal hRe)
@@ -599,7 +596,7 @@
lemma HComplex_add [simp]:
"HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
-by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib)
+by (simp add: HComplex_def add_ac right_distrib)
lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
by (simp add: HComplex_def hcomplex_of_hypreal_minus)
@@ -611,7 +608,6 @@
lemma HComplex_mult [simp]:
"HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus
- hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric]
add_ac mult_ac right_distrib)
(*HComplex_inverse is proved below*)
@@ -1000,7 +996,9 @@
hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
apply (cases x, cases y)
-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)
+apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def
+ starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide
+ hcomplex_diff numeral_2_eq_2 complex_of_real_def i_def)
apply (simp add: diff_minus)
done
@@ -1163,8 +1161,7 @@
"hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
- hcomplex_mult cis_mult [symmetric]
- complex_of_real_mult [symmetric])
+ hcomplex_mult cis_mult [symmetric])
done
lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
@@ -1304,17 +1301,28 @@
lemma hcomplex_of_complex_inverse [simp]:
"hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
-apply (case_tac "r=0")
-apply (simp add: hcomplex_of_complex_zero)
-apply (rule_tac c1 = "hcomplex_of_complex r"
- in hcomplex_mult_left_cancel [THEN iffD1])
-apply (force simp add: hcomplex_of_complex_zero_iff)
-apply (subst hcomplex_of_complex_mult [symmetric])
-apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
-done
+proof cases
+ assume "r=0" thus ?thesis by simp
+next
+ assume nz: "r\<noteq>0"
+ show ?thesis
+ proof (rule hcomplex_mult_left_cancel [THEN iffD1])
+ show "hcomplex_of_complex r \<noteq> 0"
+ by (simp add: nz)
+ next
+ have "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
+ hcomplex_of_complex (r * inverse r)"
+ by simp
+ also have "... = hcomplex_of_complex r * inverse (hcomplex_of_complex r)"
+ by (simp add: nz)
+ finally show "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
+ hcomplex_of_complex r * inverse (hcomplex_of_complex r)" .
+ qed
+qed
lemma hcomplex_of_complex_divide [simp]:
- "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
+ "hcomplex_of_complex (z1 / z2) =
+ hcomplex_of_complex z1 / hcomplex_of_complex z2"
by (simp add: hcomplex_divide_def complex_divide_def)
lemma hRe_hcomplex_of_complex:
@@ -1334,38 +1342,38 @@
instance hcomplex :: number ..
-primrec (*the type constraint is essential!*)
- number_of_Pls: "number_of bin.Pls = 0"
- number_of_Min: "number_of bin.Min = - (1::hcomplex)"
- number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
- number_of_Min [simp del]
- number_of_BIT [simp del]
+defs (overloaded)
+ hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
+ --{*the type constraint is essential!*}
instance hcomplex :: number_ring
-proof
- show "Numeral0 = (0::hcomplex)" by (rule number_of_Pls)
- show "-1 = - (1::hcomplex)" by (rule number_of_Min)
- fix w :: bin and x :: bool
- show "(number_of (w BIT x) :: hcomplex) =
- (if x then 1 else 0) + number_of w + number_of w"
- by (rule number_of_BIT)
+by (intro_classes, simp add: hcomplex_number_of_def)
+
+
+lemma hcomplex_of_complex_of_nat [simp]:
+ "hcomplex_of_complex (of_nat n) = of_nat n"
+by (induct n, simp_all)
+
+lemma hcomplex_of_complex_of_int [simp]:
+ "hcomplex_of_complex (of_int z) = of_int z"
+proof (cases z)
+ case (1 n)
+ thus ?thesis by simp
+next
+ case (2 n)
+ thus ?thesis
+ by (simp only: of_int_minus hcomplex_of_complex_minus, simp)
qed
text{*Collapse applications of @{term hcomplex_of_complex} to @{term number_of}*}
lemma hcomplex_number_of [simp]:
"hcomplex_of_complex (number_of w) = number_of w"
-apply (induct w)
-apply (simp_all only: number_of hcomplex_of_complex_add
- hcomplex_of_complex_minus, simp_all)
-done
+by (simp add: hcomplex_number_of_def complex_number_of_def)
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
"hcomplex_of_hypreal (hypreal_of_real x) =
- hcomplex_of_complex(complex_of_real x)"
+ hcomplex_of_complex (complex_of_real x)"
by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def
complex_of_real_def)
--- a/src/HOL/Hyperreal/HTranscendental.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Thu Jul 01 12:29:53 2004 +0200
@@ -9,6 +9,25 @@
theory HTranscendental = Transcendental + Integration:
+text{*really belongs in Transcendental*}
+lemma sqrt_divide_self_eq:
+ assumes nneg: "0 \<le> x"
+ shows "sqrt x / x = inverse (sqrt x)"
+proof cases
+ assume "x=0" thus ?thesis by simp
+next
+ assume nz: "x\<noteq>0"
+ hence pos: "0<x" using nneg by arith
+ show ?thesis
+ proof (rule right_inverse_eq [THEN iffD1, THEN sym])
+ show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz)
+ show "inverse (sqrt x) / (sqrt x / x) = 1"
+ by (simp add: divide_inverse mult_assoc [symmetric]
+ power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz)
+ qed
+qed
+
+
constdefs
exphr :: "real => hypreal"
--- a/src/HOL/Hyperreal/HyperArith.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy Thu Jul 01 12:29:53 2004 +0200
@@ -14,32 +14,18 @@
instance hypreal :: number ..
-primrec (*the type constraint is essential!*)
- number_of_Pls: "number_of bin.Pls = 0"
- number_of_Min: "number_of bin.Min = - (1::hypreal)"
- number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
- number_of_Min [simp del]
- number_of_BIT [simp del]
+defs (overloaded)
+ hypreal_number_of_def: "(number_of w :: hypreal) == of_int (Rep_Bin w)"
+ --{*the type constraint is essential!*}
instance hypreal :: number_ring
-proof
- show "Numeral0 = (0::hypreal)" by (rule number_of_Pls)
- show "-1 = - (1::hypreal)" by (rule number_of_Min)
- fix w :: bin and x :: bool
- show "(number_of (w BIT x) :: hypreal) =
- (if x then 1 else 0) + number_of w + number_of w"
- by (rule number_of_BIT)
-qed
+by (intro_classes, simp add: hypreal_number_of_def)
text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*}
lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
-apply (induct w)
-apply (simp_all only: number_of hypreal_of_real_add hypreal_of_real_minus, simp_all)
-done
+by (simp add: hypreal_number_of_def real_number_of_def)
+
use "hypreal_arith.ML"
--- a/src/HOL/Hyperreal/HyperDef.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Thu Jul 01 12:29:53 2004 +0200
@@ -526,6 +526,14 @@
"hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
by (simp add: hypreal_of_real_def, simp add: hypreal_add left_distrib)
+lemma hypreal_of_real_minus [simp]:
+ "hypreal_of_real (-r) = - hypreal_of_real r"
+by (auto simp add: hypreal_of_real_def hypreal_minus)
+
+lemma hypreal_of_real_diff [simp]:
+ "hypreal_of_real (w - z) = hypreal_of_real w - hypreal_of_real z"
+by (simp add: diff_minus)
+
lemma hypreal_of_real_mult [simp]:
"hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
by (simp add: hypreal_of_real_def, simp add: hypreal_mult right_distrib)
@@ -572,10 +580,6 @@
declare hypreal_of_real_le_iff [of _ 1, simplified, simp]
declare hypreal_of_real_eq_iff [of _ 1, simplified, simp]
-lemma hypreal_of_real_minus [simp]:
- "hypreal_of_real (-r) = - hypreal_of_real r"
-by (auto simp add: hypreal_of_real_def hypreal_minus)
-
lemma hypreal_of_real_inverse [simp]:
"hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
apply (case_tac "r=0", simp)
@@ -587,6 +591,19 @@
"hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z"
by (simp add: hypreal_divide_def real_divide_def)
+lemma hypreal_of_real_of_nat [simp]: "hypreal_of_real (of_nat n) = of_nat n"
+by (induct n, simp_all)
+
+lemma hypreal_of_real_of_int [simp]: "hypreal_of_real (of_int z) = of_int z"
+proof (cases z)
+ case (1 n)
+ thus ?thesis by simp
+next
+ case (2 n)
+ thus ?thesis
+ by (simp only: of_int_minus hypreal_of_real_minus, simp)
+qed
+
subsection{*Misc Others*}
--- a/src/HOL/Hyperreal/Transcendental.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Thu Jul 01 12:29:53 2004 +0200
@@ -8,42 +8,42 @@
Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim +
constdefs
- root :: [nat,real] => real
+ root :: "[nat,real] => real"
"root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
- sqrt :: real => real
+ sqrt :: "real => real"
"sqrt x == root 2 x"
- exp :: real => real
+ exp :: "real => real"
"exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"
- sin :: real => real
+ sin :: "real => real"
"sin x == suminf(%n. (if even(n) then 0 else
((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
- diffs :: (nat => real) => nat => real
+ diffs :: "(nat => real) => nat => real"
"diffs c == (%n. real (Suc n) * c(Suc n))"
- cos :: real => real
+ cos :: "real => real"
"cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n))
else 0) * x ^ n)"
- ln :: real => real
+ ln :: "real => real"
"ln x == (@u. exp u = x)"
- pi :: real
+ pi :: "real"
"pi == 2 * (@x. 0 <= (x::real) & x <= 2 & cos x = 0)"
- tan :: real => real
+ tan :: "real => real"
"tan x == (sin x)/(cos x)"
- arcsin :: real => real
+ arcsin :: "real => real"
"arcsin y == (@x. -(pi/2) <= x & x <= pi/2 & sin x = y)"
- arcos :: real => real
+ arcos :: "real => real"
"arcos y == (@x. 0 <= x & x <= pi & cos x = y)"
- arctan :: real => real
+ arctan :: "real => real"
"arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
end
--- a/src/HOL/Import/HOL/HOL4Prob.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Thu Jul 01 12:29:53 2004 +0200
@@ -27,7 +27,7 @@
((op *::nat => nat => nat)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))
q)
@@ -40,14 +40,14 @@
((op div::nat => nat => nat) n
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
((op =::nat => nat => bool) r
((op mod::nat => nat => nat) n
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))))))"
by (import prob_extra DIV_TWO_UNIQUE)
@@ -76,13 +76,13 @@
((op div::nat => nat => nat) m
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
((op div::nat => nat => nat) n
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
((op <::nat => nat => bool) m n)))"
@@ -98,13 +98,13 @@
((op div::nat => nat => nat) m
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
((op div::nat => nat => nat) n
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
((op <::nat => nat => bool) m n))))"
@@ -204,7 +204,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
n)
@@ -212,7 +212,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
m))))"
@@ -2528,7 +2528,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
((prob::((nat => bool) => bool) => real) p)))))"
@@ -3156,7 +3156,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
((size::bool list => nat) x))
@@ -3382,7 +3382,7 @@
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
(P ((Suc::nat => nat) v)))))
@@ -3436,7 +3436,7 @@
(P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
s)
@@ -3716,13 +3716,13 @@
((op ^::nat => nat => nat)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))
((unif_bound::nat => nat) n))
((op *::nat => nat => nat)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))
n)))"
by (import prob_uniform UNIF_BOUND_UPPER)
@@ -3771,7 +3771,7 @@
((op ^::nat => nat => nat)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))
((unif_bound::nat => nat) n)))
@@ -3788,7 +3788,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
((unif_bound::nat => nat) n))))))"
@@ -3907,7 +3907,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
t))))))"
@@ -3938,7 +3938,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
t)))))"
@@ -3969,7 +3969,7 @@
((op /::real => real => real) (1::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
t)))))"
--- a/src/HOL/Import/HOL/HOL4Real.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy Thu Jul 01 12:29:53 2004 +0200
@@ -1916,13 +1916,13 @@
((op *::nat => nat => nat)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))
n)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
f)
@@ -1958,7 +1958,7 @@
((number_of::bin => nat)
((op BIT::bin => bool => bin)
((op BIT::bin => bool => bin)
- (bin.Pls::bin) (True::bool))
+ (Numeral.Pls::bin) (True::bool))
(False::bool)))
d)))
(f ((op +::nat => nat => nat) n
@@ -1967,7 +1967,7 @@
((number_of::bin => nat)
((op BIT::bin => bool => bin)
((op BIT::bin => bool => bin)
- (bin.Pls::bin) (True::bool))
+ (Numeral.Pls::bin) (True::bool))
(False::bool)))
d)
(1::nat))))))))
@@ -2825,7 +2825,7 @@
((op ^::real => nat => real) ((inverse::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x))"
by (import lim DIFF_XM1)
@@ -2848,7 +2848,7 @@
((op ^::real => nat => real) (f x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))))
x))))"
@@ -2886,7 +2886,7 @@
((number_of::bin => nat)
((op BIT::bin => bool => bin)
((op BIT::bin => bool => bin)
-(bin.Pls::bin) (True::bool))
+(Numeral.Pls::bin) (True::bool))
(False::bool)))))
x))))))"
by (import lim DIFF_DIV)
@@ -3869,7 +3869,7 @@
((op -::nat => nat => nat) n
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))
p)
q)))))))))))"
@@ -3917,7 +3917,7 @@
((number_of::bin => nat)
((op BIT::bin => bool => bin)
((op BIT::bin => bool => bin)
- (bin.Pls::bin) (True::bool))
+ (Numeral.Pls::bin) (True::bool))
(False::bool)))))
((abs::real => real) h)))))))))"
by (import powser TERMDIFF_LEMMA3)
@@ -4112,7 +4112,7 @@
((op ^::real => nat => real) (f x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
x))
((op &::bool => bool => bool)
@@ -4133,7 +4133,7 @@
((op ^::real => nat => real) (g x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x))
((op &::bool => bool => bool)
@@ -4652,7 +4652,7 @@
((op ^::real => nat => real) ((sqrt::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))
x))"
by (import transc SQRT_POW_2)
@@ -4664,7 +4664,7 @@
((op ^::real => nat => real) x
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x)"
by (import transc POW_2_SQRT)
@@ -4682,7 +4682,7 @@
((op ^::real => nat => real) xa
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
x)))
@@ -4746,18 +4746,18 @@
((op ^::real => nat => real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))
n))
((op ^::real => nat => real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))
((op div::nat => nat => nat) n
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))))"
by (import transc SQRT_EVEN_POW2)
@@ -4780,7 +4780,7 @@
((op ^::real => nat => real) x
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))
y)
@@ -4848,7 +4848,7 @@
((op <::real => real => bool) x
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
by (import transc SIN_POS)
@@ -4923,7 +4923,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
by (import transc SIN_POS_PI2)
@@ -4937,7 +4937,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI2)
@@ -4951,14 +4951,14 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x)
((op <::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI)
@@ -4981,7 +4981,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI2_LE)
@@ -4995,14 +4995,14 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x)
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
by (import transc COS_POS_PI_LE)
@@ -5016,7 +5016,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op <=::real => real => bool) (0::real) ((sin::real => real) x)))"
by (import transc SIN_POS_PI2_LE)
@@ -5059,7 +5059,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
x)
@@ -5068,7 +5068,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
((op =::real => real => bool) ((sin::real => real) x) y)))))"
@@ -5089,7 +5089,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))))))"
by (import transc COS_ZERO_LEMMA)
@@ -5108,7 +5108,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))))))"
by (import transc SIN_ZERO_LEMMA)
@@ -5186,7 +5186,7 @@
((op *::real => real => real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))
x))
@@ -5196,21 +5196,21 @@
((op *::real => real => real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))
x))
((op /::real => real => real)
((op *::real => real => real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))
((tan::real => real) x))
((op -::real => real => real) (1::real)
((op ^::real => nat => real) ((tan::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))))"
by (import transc TAN_DOUBLE)
@@ -5223,7 +5223,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op <::real => real => bool) (0::real) ((tan::real => real) x)))"
by (import transc TAN_POS_PI2)
@@ -5238,7 +5238,7 @@
((op ^::real => nat => real) ((cos::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x))"
by (import transc DIFF_TAN)
@@ -5256,7 +5256,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
((op <::real => real => bool) y ((tan::real => real) x))))))"
@@ -5275,7 +5275,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))
((op =::real => real => bool) ((tan::real => real) x) y)))))"
@@ -5317,7 +5317,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
((asn::real => real) y))
((op &::bool => bool => bool)
@@ -5325,7 +5325,7 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
((op =::real => real => bool)
((sin::real => real) ((asn::real => real) y)) y))))"
@@ -5353,14 +5353,14 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
((asn::real => real) y))
((op <=::real => real => bool) ((asn::real => real) y)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))))"
by (import transc ASN_BOUNDS)
@@ -5376,14 +5376,14 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
((asn::real => real) y))
((op <::real => real => bool) ((asn::real => real) y)
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))))"
by (import transc ASN_BOUNDS_LT)
@@ -5396,14 +5396,14 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x)
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op =::real => real => bool)
((asn::real => real) ((sin::real => real) x)) x))"
@@ -5483,14 +5483,14 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x)
((op <::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op =::real => real => bool)
((atn::real => real) ((tan::real => real) x)) x))"
@@ -5506,13 +5506,13 @@
((op ^::real => nat => real) ((tan::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
((op ^::real => nat => real)
((inverse::real => real) ((cos::real => real) x))
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))"
by (import transc TAN_SEC)
@@ -5528,7 +5528,7 @@
((op ^::real => nat => real) ((cos::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))))"
by (import transc SIN_COS_SQ)
@@ -5541,14 +5541,14 @@
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool)))))
x)
((op <=::real => real => bool) x
((op /::real => real => real) (pi::real)
((number_of::bin => real)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))
((op =::real => real => bool) ((cos::real => real) x)
((sqrt::real => real)
@@ -5556,7 +5556,7 @@
((op ^::real => nat => real) ((sin::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))))"
by (import transc COS_SIN_SQ)
@@ -5595,7 +5595,7 @@
((op ^::real => nat => real) ((sin::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))))"
by (import transc COS_SIN_SQRT)
@@ -5609,7 +5609,7 @@
((op ^::real => nat => real) ((cos::real => real) x)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))))))"
by (import transc SIN_COS_SQRT)
@@ -5646,7 +5646,7 @@
((op ^::real => nat => real) x
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))))))
x))"
@@ -5679,7 +5679,7 @@
((op ^::real => nat => real) x
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool))))))))
x))"
--- a/src/HOL/Import/HOL/HOL4Vec.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Thu Jul 01 12:29:53 2004 +0200
@@ -1103,7 +1103,7 @@
((op <::nat => nat => bool) x
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
(False::bool))))
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
x))"
@@ -1298,7 +1298,7 @@
((op ^::nat => nat => nat)
((number_of::bin => nat)
((op BIT::bin => bool => bin)
- ((op BIT::bin => bool => bin) (bin.Pls::bin)
+ ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
(True::bool))
(False::bool)))
k)))))))"
--- a/src/HOL/Integ/Bin.thy Wed Jun 30 14:04:58 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-(* Title: HOL/Integ/Bin.thy
- ID: $Id$
- Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Ported from ZF to HOL by David Spelt.
-*)
-
-header{*Arithmetic on Binary Integers*}
-
-theory Bin = IntDef + Numeral:
-
-axclass number_ring \<subseteq> number, comm_ring_1
- number_of_Pls: "number_of bin.Pls = 0"
- number_of_Min: "number_of bin.Min = - 1"
- number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
-subsection{*Converting Numerals to Rings: @{term number_of}*}
-
-lemmas number_of = number_of_Pls number_of_Min number_of_BIT
-
-lemma number_of_NCons [simp]:
- "number_of(NCons w b) = (number_of(w BIT b)::'a::number_ring)"
-by (induct_tac "w", simp_all add: number_of)
-
-lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all add: number_of add_ac)
-done
-
-lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all add: number_of add_assoc [symmetric])
-done
-
-lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all del: bin_pred_Pls bin_pred_Min bin_pred_BIT
- add: number_of number_of_succ number_of_pred add_assoc)
-done
-
-text{*This proof is complicated by the mutual recursion*}
-lemma number_of_add [rule_format]:
- "\<forall>w. number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
-apply (induct_tac "v")
-apply (simp add: number_of)
-apply (simp add: number_of number_of_pred)
-apply (rule allI)
-apply (induct_tac "w")
-apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac)
-done
-
-lemma number_of_mult:
- "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
-apply (induct_tac "v", simp add: number_of)
-apply (simp add: number_of number_of_minus)
-apply (simp add: number_of number_of_add left_distrib add_ac)
-done
-
-text{*The correctness of shifting. But it doesn't seem to give a measurable
- speed-up.*}
-lemma double_number_of_BIT:
- "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all add: number_of number_of_add left_distrib add_ac)
-done
-
-
-text{*Converting numerals 0 and 1 to their abstract versions*}
-lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
-by (simp add: number_of)
-
-lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
-by (simp add: number_of)
-
-text{*Special-case simplification for small constants*}
-
-text{*Unary minus for the abstract constant 1. Cannot be inserted
- as a simprule until later: it is @{text number_of_Min} re-oriented!*}
-lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
-by (simp add: number_of)
-
-lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
-
-lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
-
-(*Negation of a coefficient*)
-lemma minus_number_of_mult [simp]:
- "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
-by (simp add: number_of_minus)
-
-text{*Subtraction*}
-lemma diff_number_of_eq:
- "number_of v - number_of w =
- (number_of(bin_add v (bin_minus w))::'a::number_ring)"
-by (simp add: diff_minus number_of_add number_of_minus)
-
-
-subsection{*Equality of Binary Numbers*}
-
-text{*First version by Norbert Voelker*}
-
-lemma eq_number_of_eq:
- "((number_of x::'a::number_ring) = number_of y) =
- iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
-by (simp add: iszero_def compare_rls number_of_add number_of_minus)
-
-lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::'a::number_ring)"
-by (simp add: iszero_def numeral_0_eq_0)
-
-lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::'a::number_ring)"
-by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
-
-
-subsection{*Comparisons, for Ordered Rings*}
-
-lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
-proof -
- have "a + a = (1+1)*a" by (simp add: left_distrib)
- with zero_less_two [where 'a = 'a]
- show ?thesis by force
-qed
-
-lemma le_imp_0_less:
- assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
-proof -
- have "0 \<le> z" .
- also have "... < z + 1" by (rule less_add_one)
- also have "... = 1 + z" by (simp add: add_ac)
- finally show "0 < 1 + z" .
-qed
-
-lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
-proof (cases z rule: int_cases)
- case (nonneg n)
- have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
- thus ?thesis using le_imp_0_less [OF le]
- by (auto simp add: add_assoc)
-next
- case (neg n)
- show ?thesis
- proof
- assume eq: "1 + z + z = 0"
- have "0 < 1 + (int n + int n)"
- by (simp add: le_imp_0_less add_increasing)
- also have "... = - (1 + z + z)"
- by (simp add: neg add_assoc [symmetric])
- also have "... = 0" by (simp add: eq)
- finally have "0<0" ..
- thus False by blast
- qed
-qed
-
-
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
-lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
-proof (unfold Ints_def)
- assume "a \<in> range of_int"
- then obtain z where a: "a = of_int z" ..
- show ?thesis
- proof
- assume eq: "1 + a + a = 0"
- hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
- hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
- with odd_nonzero show False by blast
- qed
-qed
-
-lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
-by (induct_tac "w", simp_all add: number_of)
-
-lemma iszero_number_of_BIT:
- "iszero (number_of (w BIT x)::'a) =
- (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
-by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff
- number_of Ints_odd_nonzero [OF Ints_number_of])
-
-lemma iszero_number_of_0:
- "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) =
- iszero (number_of w :: 'a)"
-by (simp only: iszero_number_of_BIT simp_thms)
-
-lemma iszero_number_of_1:
- "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
-by (simp only: iszero_number_of_BIT simp_thms)
-
-
-
-subsection{*The Less-Than Relation*}
-
-lemma less_number_of_eq_neg:
- "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
- = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
-apply (subst less_iff_diff_less_0)
-apply (simp add: neg_def diff_minus number_of_add number_of_minus)
-done
-
-text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
- @{term Numeral0} IS @{term "number_of Pls"} *}
-lemma not_neg_number_of_Pls:
- "~ neg (number_of bin.Pls ::'a::{ordered_idom,number_ring})"
-by (simp add: neg_def numeral_0_eq_0)
-
-lemma neg_number_of_Min:
- "neg (number_of bin.Min ::'a::{ordered_idom,number_ring})"
-by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
-
-lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
-proof -
- have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
- also have "... = (a < 0)"
- by (simp add: mult_less_0_iff zero_less_two
- order_less_not_sym [OF zero_less_two])
- finally show ?thesis .
-qed
-
-lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
-proof (cases z rule: int_cases)
- case (nonneg n)
- thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
- le_imp_0_less [THEN order_less_imp_le])
-next
- case (neg n)
- thus ?thesis by (simp del: int_Suc
- add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
-qed
-
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
-lemma Ints_odd_less_0:
- "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
-proof (unfold Ints_def)
- assume "a \<in> range of_int"
- then obtain z where a: "a = of_int z" ..
- hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
- by (simp add: a)
- also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
- also have "... = (a < 0)" by (simp add: a)
- finally show ?thesis .
-qed
-
-lemma neg_number_of_BIT:
- "neg (number_of (w BIT x)::'a) =
- neg (number_of w :: 'a::{ordered_idom,number_ring})"
-by (simp add: number_of neg_def double_less_0_iff
- Ints_odd_less_0 [OF Ints_number_of])
-
-
-text{*Less-Than or Equals*}
-
-text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
-lemmas le_number_of_eq_not_less =
- linorder_not_less [of "number_of w" "number_of v", symmetric,
- standard]
-
-lemma le_number_of_eq:
- "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
- = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
-by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
-
-
-text{*Absolute value (@{term abs})*}
-
-lemma abs_number_of:
- "abs(number_of x::'a::{ordered_idom,number_ring}) =
- (if number_of x < (0::'a) then -number_of x else number_of x)"
-by (simp add: abs_if)
-
-
-text{*Re-orientation of the equation nnn=x*}
-lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
-by auto
-
-
-(*Delete the original rewrites, with their clumsy conditional expressions*)
-declare bin_succ_BIT [simp del] bin_pred_BIT [simp del]
- bin_minus_BIT [simp del]
-
-declare bin_add_BIT [simp del] bin_mult_BIT [simp del]
-declare NCons_Pls [simp del] NCons_Min [simp del]
-
-(*Hide the binary representation of integer constants*)
-declare number_of_Pls [simp del] number_of_Min [simp del]
- number_of_BIT [simp del]
-
-
-
-(*Simplification of arithmetic operations on integer constants.
- Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
-
-lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
-
-lemmas bin_arith_extra_simps =
- number_of_add [symmetric]
- number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
- number_of_mult [symmetric]
- bin_succ_1 bin_succ_0
- bin_pred_1 bin_pred_0
- bin_minus_1 bin_minus_0
- bin_add_Pls_right bin_add_Min_right
- bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
- diff_number_of_eq abs_number_of abs_zero abs_one
- bin_mult_1 bin_mult_0 NCons_simps
-
-(*For making a minimal simpset, one must include these default simprules
- of thy. Also include simp_thms, or at least (~False)=True*)
-lemmas bin_arith_simps =
- bin_pred_Pls bin_pred_Min
- bin_succ_Pls bin_succ_Min
- bin_add_Pls bin_add_Min
- bin_minus_Pls bin_minus_Min
- bin_mult_Pls bin_mult_Min bin_arith_extra_simps
-
-(*Simplification of relational operations*)
-lemmas bin_rel_simps =
- eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
- iszero_number_of_0 iszero_number_of_1
- less_number_of_eq_neg
- not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
- neg_number_of_Min neg_number_of_BIT
- le_number_of_eq
-
-declare bin_arith_extra_simps [simp]
-declare bin_rel_simps [simp]
-
-
-subsection{*Simplification of arithmetic when nested to the right*}
-
-lemma add_number_of_left [simp]:
- "number_of v + (number_of w + z) =
- (number_of(bin_add v w) + z::'a::number_ring)"
-by (simp add: add_assoc [symmetric])
-
-lemma mult_number_of_left [simp]:
- "number_of v * (number_of w * z) =
- (number_of(bin_mult v w) * z::'a::number_ring)"
-by (simp add: mult_assoc [symmetric])
-
-lemma add_number_of_diff1:
- "number_of v + (number_of w - c) =
- number_of(bin_add v w) - (c::'a::number_ring)"
-by (simp add: diff_minus add_number_of_left)
-
-lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
- number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
-apply (subst diff_number_of_eq [symmetric])
-apply (simp only: compare_rls)
-done
-
-end
--- a/src/HOL/Integ/IntArith.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/IntArith.thy Thu Jul 01 12:29:53 2004 +0200
@@ -5,7 +5,7 @@
header {* Integer arithmetic *}
-theory IntArith = Bin
+theory IntArith = Numeral
files ("int_arith1.ML"):
text{*Duplicate: can't understand why it's necessary*}
@@ -16,26 +16,12 @@
instance
int :: number ..
-primrec (*the type constraint is essential!*)
- number_of_Pls: "number_of bin.Pls = 0"
- number_of_Min: "number_of bin.Min = - (1::int)"
- number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
- number_of_Min [simp del]
- number_of_BIT [simp del]
+defs (overloaded)
+ int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)"
+ --{*the type constraint is essential!*}
instance int :: number_ring
-proof
- show "Numeral0 = (0::int)" by (rule number_of_Pls)
- show "-1 = - (1::int)" by (rule number_of_Min)
- fix w :: bin and x :: bool
- show "(number_of (w BIT x) :: int) =
- (if x then 1 else 0) + number_of w + number_of w"
- by (rule number_of_BIT)
-qed
-
+by (intro_classes, simp add: int_number_of_def)
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
@@ -135,9 +121,7 @@
lemma of_int_number_of_eq:
"of_int (number_of v) = (number_of v :: 'a :: number_ring)"
-apply (induct v)
-apply (simp_all only: number_of of_int_add, simp_all)
-done
+by (simp add: number_of_eq)
text{*Lemmas for specialist use, NOT as default simprules*}
lemma mult_2: "2 * z = (z+z::'a::number_ring)"
@@ -210,7 +194,7 @@
(*Analogous to zadd_int*)
-lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
+lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
by (induct m n rule: diff_induct, simp_all)
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
--- a/src/HOL/Integ/IntDef.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy Thu Jul 01 12:29:53 2004 +0200
@@ -810,10 +810,9 @@
lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
by (induct n, auto)
-lemma of_int_int_eq [simp]: "of_int (int n) = int n"
+lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
by (simp add: int_eq_of_nat)
-
lemma Ints_cases [case_names of_int, cases set: Ints]:
"q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C"
proof (simp add: Ints_def)
@@ -922,6 +921,12 @@
by (cases z) auto
+lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
+apply (cases z)
+apply (simp_all add: not_zle_0_negative del: int_Suc)
+done
+
+
(*Legacy ML bindings, but no longer the structure Int.*)
ML
{*
--- a/src/HOL/Integ/IntDiv.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy Thu Jul 01 12:29:53 2004 +0200
@@ -221,7 +221,7 @@
(** Basic laws about division and remainder **)
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (cut_tac a = a and b = b in divAlg_correct)
apply (auto simp add: quorem_def div_def mod_def)
done
@@ -302,7 +302,7 @@
(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (simp add: quorem_div_mod [THEN quorem_neg, simplified,
THEN quorem_div, THEN sym])
@@ -310,7 +310,7 @@
(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod],
auto)
done
@@ -332,7 +332,7 @@
lemma zmod_zminus1_eq_if:
"(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod])
done
@@ -384,7 +384,7 @@
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
lemma zmod_self [simp]: "a mod a = (0::int)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
apply (simp add: quorem_div_mod [THEN self_remainder])
done
@@ -588,12 +588,12 @@
by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
done
lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
done
@@ -642,22 +642,22 @@
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
lemma zdiv_zadd1_eq:
"(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
done
lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
done
lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
done
lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
done
@@ -680,12 +680,12 @@
by (simp add: zdiv_zadd1_eq)
lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
apply (simp add: zmod_zadd1_eq)
done
lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
apply (simp add: zmod_zadd1_eq)
done
@@ -737,13 +737,13 @@
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div])
done
lemma zmod_zmult2_eq:
"(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod])
done
@@ -759,7 +759,7 @@
done
lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
done
@@ -781,8 +781,8 @@
done
lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
+apply (case_tac "c = 0", simp)
apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
done
@@ -832,7 +832,7 @@
(0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
(k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
apply (case_tac "k=0")
- apply (simp add: DIVISION_BY_ZERO)
+ apply (simp)
apply (simp only: linorder_neq_iff)
apply (erule disjE)
apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
@@ -845,7 +845,7 @@
(0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
(k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
apply (case_tac "k=0")
- apply (simp add: DIVISION_BY_ZERO)
+ apply (simp)
apply (simp only: linorder_neq_iff)
apply (erule disjE)
apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
@@ -904,20 +904,16 @@
(if ~b | (0::int) \<le> number_of w
then number_of v div (number_of w)
else (number_of v + (1::int)) div (number_of w))"
-apply (simp only: add_assoc number_of_BIT)
-(*create subgoal because the next step can't simplify numerals*)
-apply (subgoal_tac "2 ~= (0::int) ")
-apply (simp del: bin_arith_extra_simps arith_special
- add: zdiv_zmult_zmult1 pos_zdiv_mult_2 not_0_le_lemma neg_zdiv_mult_2)
-apply simp
+apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if)
+apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
done
-(** computing mod by shifting (proofs resemble those for div) **)
+subsection{*Computing mod by Shifting (proofs resemble those for div)*}
lemma pos_zmod_mult_2:
"(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
apply (subgoal_tac "1 \<le> a")
prefer 2 apply arith
apply (subgoal_tac "1 < a * 2")
@@ -952,15 +948,14 @@
then 2 * (number_of v mod number_of w) + 1
else 2 * ((number_of v + (1::int)) mod number_of w) - 1
else 2 * (number_of v mod number_of w))"
-apply (simp only: zadd_assoc number_of_BIT)
-apply (simp del: bin_arith_extra_simps bin_rel_simps arith_special
- add: zmod_zmult_zmult1 pos_zmod_mult_2 not_0_le_lemma neg_zmod_mult_2
- neg_def)
+apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if)
+apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
+ not_0_le_lemma neg_zmod_mult_2 add_ac)
done
-(** Quotients of signs **)
+subsection{*Quotients of Signs*}
lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"
apply (subgoal_tac "a div b \<le> -1", force)
--- a/src/HOL/Integ/NatBin.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy Thu Jul 01 12:29:53 2004 +0200
@@ -478,8 +478,8 @@
lemma eq_number_of_BIT_Pls:
- "((number_of (v BIT x) ::int) = number_of bin.Pls) =
- (x=False & (((number_of v) ::int) = number_of bin.Pls))"
+ "((number_of (v BIT x) ::int) = Numeral0) =
+ (x=False & (((number_of v) ::int) = Numeral0))"
apply (simp only: simp_thms add: number_of_BIT number_of_Pls eq_commute
split add: split_if cong: imp_cong)
apply (rule_tac x = "number_of v" in spec, safe)
@@ -489,15 +489,15 @@
done
lemma eq_number_of_BIT_Min:
- "((number_of (v BIT x) ::int) = number_of bin.Min) =
- (x=True & (((number_of v) ::int) = number_of bin.Min))"
+ "((number_of (v BIT x) ::int) = number_of Numeral.Min) =
+ (x=True & (((number_of v) ::int) = number_of Numeral.Min))"
apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute
split add: split_if cong: imp_cong)
apply (rule_tac x = "number_of v" in spec, auto)
apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
done
-lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min"
+lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Numeral.Min"
by auto
@@ -569,10 +569,10 @@
declare split_div[of _ _ "number_of k", standard, arith_split]
declare split_mod[of _ _ "number_of k", standard, arith_split]
-lemma nat_number_of_Pls: "number_of bin.Pls = (0::nat)"
+lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
by (simp add: number_of_Pls nat_number_of_def)
-lemma nat_number_of_Min: "number_of bin.Min = (0::nat)"
+lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
apply (simp add: neg_nat)
done
@@ -622,23 +622,12 @@
lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
by (simp only: nat_number_of_def, simp)
-lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
-by arith
-
lemma of_nat_number_of_lemma:
"of_nat (number_of v :: nat) =
(if 0 \<le> (number_of v :: int)
then (number_of v :: 'a :: number_ring)
else 0)"
-apply (induct v, simp, simp add: nat_numeral_m1_eq_0)
-apply (simp only: number_of nat_number_of_def)
-txt{*Generalize in order to eliminate the function @{term number_of} and
-its annoying simprules*}
-apply (erule rev_mp)
-apply (rule_tac x="number_of bin :: int" in spec)
-apply (rule_tac x="number_of bin :: 'a" in spec)
-apply (simp add: nat_add_distrib of_nat_double int_double_iff)
-done
+by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
lemma of_nat_number_of_eq [simp]:
"of_nat (number_of v :: nat) =
@@ -850,6 +839,8 @@
"uminus" :: "int => int" ("`~")
"op +" :: "int => int => int" ("(_ `+/ _)")
"op *" :: "int => int => int" ("(_ `*/ _)")
+ "op div" :: "int => int => int" ("(_ `div/ _)")
+ "op mod" :: "int => int => int" ("(_ `mod/ _)")
"op <" :: "int => int => bool" ("(_ </ _)")
"op <=" :: "int => int => bool" ("(_ <=/ _)")
"neg" ("(_ < 0)")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Numeral.thy Thu Jul 01 12:29:53 2004 +0200
@@ -0,0 +1,505 @@
+(* Title: HOL/Integ/Numeral.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+*)
+
+header{*Arithmetic on Binary Integers*}
+
+theory Numeral = IntDef
+files "Tools/numeral_syntax.ML":
+
+text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
+ Only qualified access Numeral.Pls and Numeral.Min is allowed.
+ We do not hide Bit because we need the BIT infix syntax.*}
+
+text{*This formalization defines binary arithmetic in terms of the integers
+rather than using a datatype. This avoids multiple representations (leading
+zeroes, etc.) See @{text "ZF/Integ/twos-compl.ML"}, function @{text
+int_of_binary}, for the numerical interpretation.
+
+The representation expects that @{text "(m mod 2)"} is 0 or 1,
+even if m is negative;
+For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
+@{text "-5 = (-3)*2 + 1"}.
+*}
+
+
+typedef (Bin)
+ bin = "UNIV::int set"
+ by (auto)
+
+constdefs
+ Pls :: "bin"
+ "Pls == Abs_Bin 0"
+
+ Min :: "bin"
+ "Min == Abs_Bin (- 1)"
+
+ Bit :: "[bin,bool] => bin" (infixl "BIT" 90)
+ --{*That is, 2w+b*}
+ "w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
+
+
+axclass
+ number < type -- {* for numeric types: nat, int, real, \dots *}
+
+consts
+ number_of :: "bin => 'a::number"
+
+syntax
+ "_Numeral" :: "num_const => 'a" ("_")
+ Numeral0 :: 'a
+ Numeral1 :: 'a
+
+translations
+ "Numeral0" == "number_of Numeral.Pls"
+ "Numeral1" == "number_of (Numeral.Pls BIT True)"
+
+
+setup NumeralSyntax.setup
+
+syntax (xsymbols)
+ "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
+syntax (HTML output)
+ "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
+syntax (output)
+ "_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
+translations
+ "x\<twosuperior>" == "x^2"
+ "x\<twosuperior>" <= "x^(2::nat)"
+
+
+lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
+ -- {* Unfold all @{text let}s involving constants *}
+ by (simp add: Let_def)
+
+lemma Let_0 [simp]: "Let 0 f == f 0"
+ by (simp add: Let_def)
+
+lemma Let_1 [simp]: "Let 1 f == f 1"
+ by (simp add: Let_def)
+
+
+constdefs
+ bin_succ :: "bin=>bin"
+ "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
+
+ bin_pred :: "bin=>bin"
+ "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
+
+ bin_minus :: "bin=>bin"
+ "bin_minus w == Abs_Bin(- (Rep_Bin w))"
+
+ bin_add :: "[bin,bin]=>bin"
+ "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
+
+ bin_mult :: "[bin,bin]=>bin"
+ "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
+
+
+lemmas Bin_simps =
+ bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
+ Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
+
+text{*Removal of leading zeroes*}
+lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
+by (simp add: Bin_simps)
+
+lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
+by (simp add: Bin_simps)
+
+subsection{*The Functions @{term bin_succ}, @{term bin_pred} and @{term bin_minus}*}
+
+lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
+by (simp add: Bin_simps)
+
+lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
+by (simp add: Bin_simps)
+
+lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
+by (simp add: Bin_simps)
+
+lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
+by (simp add: Bin_simps diff_minus)
+
+lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
+by (simp add: Bin_simps)
+
+lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
+by (simp add: Bin_simps diff_minus add_ac)
+
+lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
+by (simp add: Bin_simps)
+
+lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
+by (simp add: Bin_simps)
+
+lemma bin_minus_1 [simp]:
+ "bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
+by (simp add: Bin_simps add_ac diff_minus)
+
+ lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
+by (simp add: Bin_simps)
+
+
+subsection{*Binary Addition and Multiplication:
+ @{term bin_add} and @{term bin_mult}*}
+
+lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
+by (simp add: Bin_simps)
+
+lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
+by (simp add: Bin_simps diff_minus add_ac)
+
+lemma bin_add_BIT_11 [simp]:
+ "bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_add_BIT_10 [simp]:
+ "bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_add_BIT_0 [simp]:
+ "bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
+by (simp add: Bin_simps)
+
+lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
+by (simp add: Bin_simps diff_minus)
+
+lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
+by (simp add: Bin_simps)
+
+lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
+by (simp add: Bin_simps)
+
+lemma bin_mult_1 [simp]:
+ "bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
+by (simp add: Bin_simps add_ac left_distrib)
+
+lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
+by (simp add: Bin_simps left_distrib)
+
+
+
+subsection{*Converting Numerals to Rings: @{term number_of}*}
+
+axclass number_ring \<subseteq> number, comm_ring_1
+ number_of_eq: "number_of w = of_int (Rep_Bin w)"
+
+lemma number_of_succ:
+ "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_pred:
+ "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_minus:
+ "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_add:
+ "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_mult:
+ "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+text{*The correctness of shifting. But it doesn't seem to give a measurable
+ speed-up.*}
+lemma double_number_of_BIT:
+ "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps left_distrib)
+
+text{*Converting numerals 0 and 1 to their abstract versions*}
+lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+text{*Special-case simplification for small constants*}
+
+text{*Unary minus for the abstract constant 1. Cannot be inserted
+ as a simprule until later: it is @{text number_of_Min} re-oriented!*}
+lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
+by (simp add: number_of_eq Bin_simps)
+
+
+lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
+by (simp add: numeral_m1_eq_minus_1)
+
+lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
+by (simp add: numeral_m1_eq_minus_1)
+
+(*Negation of a coefficient*)
+lemma minus_number_of_mult [simp]:
+ "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
+by (simp add: number_of_minus)
+
+text{*Subtraction*}
+lemma diff_number_of_eq:
+ "number_of v - number_of w =
+ (number_of(bin_add v (bin_minus w))::'a::number_ring)"
+by (simp add: diff_minus number_of_add number_of_minus)
+
+
+lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_BIT:
+ "number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
+ (number_of w) + (number_of w)"
+by (simp add: number_of_eq Bin_simps)
+
+
+
+subsection{*Equality of Binary Numbers*}
+
+text{*First version by Norbert Voelker*}
+
+lemma eq_number_of_eq:
+ "((number_of x::'a::number_ring) = number_of y) =
+ iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
+by (simp add: iszero_def compare_rls number_of_add number_of_minus)
+
+lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
+by (simp add: iszero_def numeral_0_eq_0)
+
+lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
+by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
+
+
+subsection{*Comparisons, for Ordered Rings*}
+
+lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
+proof -
+ have "a + a = (1+1)*a" by (simp add: left_distrib)
+ with zero_less_two [where 'a = 'a]
+ show ?thesis by force
+qed
+
+lemma le_imp_0_less:
+ assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
+proof -
+ have "0 \<le> z" .
+ also have "... < z + 1" by (rule less_add_one)
+ also have "... = 1 + z" by (simp add: add_ac)
+ finally show "0 < 1 + z" .
+qed
+
+lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
+proof (cases z rule: int_cases)
+ case (nonneg n)
+ have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
+ thus ?thesis using le_imp_0_less [OF le]
+ by (auto simp add: add_assoc)
+next
+ case (neg n)
+ show ?thesis
+ proof
+ assume eq: "1 + z + z = 0"
+ have "0 < 1 + (int n + int n)"
+ by (simp add: le_imp_0_less add_increasing)
+ also have "... = - (1 + z + z)"
+ by (simp add: neg add_assoc [symmetric])
+ also have "... = 0" by (simp add: eq)
+ finally have "0<0" ..
+ thus False by blast
+ qed
+qed
+
+
+text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
+lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
+proof (unfold Ints_def)
+ assume "a \<in> range of_int"
+ then obtain z where a: "a = of_int z" ..
+ show ?thesis
+ proof
+ assume eq: "1 + a + a = 0"
+ hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
+ hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
+ with odd_nonzero show False by blast
+ qed
+qed
+
+lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
+by (simp add: number_of_eq Ints_def)
+
+
+lemma iszero_number_of_BIT:
+ "iszero (number_of (w BIT x)::'a) =
+ (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
+by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff
+ Ints_odd_nonzero Ints_def)
+
+lemma iszero_number_of_0:
+ "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) =
+ iszero (number_of w :: 'a)"
+by (simp only: iszero_number_of_BIT simp_thms)
+
+lemma iszero_number_of_1:
+ "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
+by (simp only: iszero_number_of_BIT simp_thms)
+
+
+
+subsection{*The Less-Than Relation*}
+
+lemma less_number_of_eq_neg:
+ "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
+ = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
+apply (subst less_iff_diff_less_0)
+apply (simp add: neg_def diff_minus number_of_add number_of_minus)
+done
+
+text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+ @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
+lemma not_neg_number_of_Pls:
+ "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
+by (simp add: neg_def numeral_0_eq_0)
+
+lemma neg_number_of_Min:
+ "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
+by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
+
+lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
+proof -
+ have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
+ also have "... = (a < 0)"
+ by (simp add: mult_less_0_iff zero_less_two
+ order_less_not_sym [OF zero_less_two])
+ finally show ?thesis .
+qed
+
+lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
+proof (cases z rule: int_cases)
+ case (nonneg n)
+ thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
+ le_imp_0_less [THEN order_less_imp_le])
+next
+ case (neg n)
+ thus ?thesis by (simp del: int_Suc
+ add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
+qed
+
+text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
+lemma Ints_odd_less_0:
+ "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
+proof (unfold Ints_def)
+ assume "a \<in> range of_int"
+ then obtain z where a: "a = of_int z" ..
+ hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
+ by (simp add: a)
+ also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
+ also have "... = (a < 0)" by (simp add: a)
+ finally show ?thesis .
+qed
+
+lemma neg_number_of_BIT:
+ "neg (number_of (w BIT x)::'a) =
+ neg (number_of w :: 'a::{ordered_idom,number_ring})"
+by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
+ Ints_odd_less_0 Ints_def)
+
+
+text{*Less-Than or Equals*}
+
+text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
+lemmas le_number_of_eq_not_less =
+ linorder_not_less [of "number_of w" "number_of v", symmetric,
+ standard]
+
+lemma le_number_of_eq:
+ "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
+ = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
+by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
+
+
+text{*Absolute value (@{term abs})*}
+
+lemma abs_number_of:
+ "abs(number_of x::'a::{ordered_idom,number_ring}) =
+ (if number_of x < (0::'a) then -number_of x else number_of x)"
+by (simp add: abs_if)
+
+
+text{*Re-orientation of the equation nnn=x*}
+lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
+by auto
+
+
+
+
+subsection{*Simplification of arithmetic operations on integer constants.*}
+
+lemmas bin_arith_extra_simps =
+ number_of_add [symmetric]
+ number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
+ number_of_mult [symmetric]
+ diff_number_of_eq abs_number_of
+
+text{*For making a minimal simpset, one must include these default simprules.
+ Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
+lemmas bin_arith_simps =
+ Pls_0_eq Min_1_eq
+ bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
+ bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
+ bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
+ bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
+ bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
+ bin_add_Pls_right bin_add_Min_right
+ abs_zero abs_one bin_arith_extra_simps
+
+text{*Simplification of relational operations*}
+lemmas bin_rel_simps =
+ eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
+ iszero_number_of_0 iszero_number_of_1
+ less_number_of_eq_neg
+ not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
+ neg_number_of_Min neg_number_of_BIT
+ le_number_of_eq
+
+declare bin_arith_extra_simps [simp]
+declare bin_rel_simps [simp]
+
+
+subsection{*Simplification of arithmetic when nested to the right*}
+
+lemma add_number_of_left [simp]:
+ "number_of v + (number_of w + z) =
+ (number_of(bin_add v w) + z::'a::number_ring)"
+by (simp add: add_assoc [symmetric])
+
+lemma mult_number_of_left [simp]:
+ "number_of v * (number_of w * z) =
+ (number_of(bin_mult v w) * z::'a::number_ring)"
+by (simp add: mult_assoc [symmetric])
+
+lemma add_number_of_diff1:
+ "number_of v + (number_of w - c) =
+ number_of(bin_add v w) - (c::'a::number_ring)"
+by (simp add: diff_minus add_number_of_left)
+
+lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
+ number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
+apply (subst diff_number_of_eq [symmetric])
+apply (simp only: compare_rls)
+done
+
+end
--- a/src/HOL/Integ/Presburger.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy Thu Jul 01 12:29:53 2004 +0200
@@ -969,7 +969,7 @@
theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
by simp
-theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
+theorem number_of2: "(0::int) <= Numeral0" by simp
theorem Suc_plus1: "Suc n = n + 1" by simp
--- a/src/HOL/Integ/int_arith1.ML Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/int_arith1.ML Thu Jul 01 12:29:53 2004 +0200
@@ -7,49 +7,37 @@
(** Misc ML bindings **)
-val NCons_Pls = thm"NCons_Pls";
-val NCons_Min = thm"NCons_Min";
-val NCons_BIT = thm"NCons_BIT";
-val number_of_Pls = thm"number_of_Pls";
-val number_of_Min = thm"number_of_Min";
-val number_of_BIT = thm"number_of_BIT";
val bin_succ_Pls = thm"bin_succ_Pls";
val bin_succ_Min = thm"bin_succ_Min";
-val bin_succ_BIT = thm"bin_succ_BIT";
+val bin_succ_1 = thm"bin_succ_1";
+val bin_succ_0 = thm"bin_succ_0";
+
val bin_pred_Pls = thm"bin_pred_Pls";
val bin_pred_Min = thm"bin_pred_Min";
-val bin_pred_BIT = thm"bin_pred_BIT";
+val bin_pred_1 = thm"bin_pred_1";
+val bin_pred_0 = thm"bin_pred_0";
+
val bin_minus_Pls = thm"bin_minus_Pls";
val bin_minus_Min = thm"bin_minus_Min";
-val bin_minus_BIT = thm"bin_minus_BIT";
+val bin_minus_1 = thm"bin_minus_1";
+val bin_minus_0 = thm"bin_minus_0";
+
val bin_add_Pls = thm"bin_add_Pls";
val bin_add_Min = thm"bin_add_Min";
-val bin_mult_Pls = thm"bin_mult_Pls";
-val bin_mult_Min = thm"bin_mult_Min";
-val bin_mult_BIT = thm"bin_mult_BIT";
-
-val neg_def = thm "neg_def";
-val iszero_def = thm "iszero_def";
-
-val NCons_Pls_0 = thm"NCons_Pls_0";
-val NCons_Pls_1 = thm"NCons_Pls_1";
-val NCons_Min_0 = thm"NCons_Min_0";
-val NCons_Min_1 = thm"NCons_Min_1";
-val bin_succ_1 = thm"bin_succ_1";
-val bin_succ_0 = thm"bin_succ_0";
-val bin_pred_1 = thm"bin_pred_1";
-val bin_pred_0 = thm"bin_pred_0";
-val bin_minus_1 = thm"bin_minus_1";
-val bin_minus_0 = thm"bin_minus_0";
val bin_add_BIT_11 = thm"bin_add_BIT_11";
val bin_add_BIT_10 = thm"bin_add_BIT_10";
val bin_add_BIT_0 = thm"bin_add_BIT_0";
val bin_add_Pls_right = thm"bin_add_Pls_right";
val bin_add_Min_right = thm"bin_add_Min_right";
-val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
+
+val bin_mult_Pls = thm"bin_mult_Pls";
+val bin_mult_Min = thm"bin_mult_Min";
val bin_mult_1 = thm"bin_mult_1";
val bin_mult_0 = thm"bin_mult_0";
-val number_of_NCons = thm"number_of_NCons";
+
+val neg_def = thm "neg_def";
+val iszero_def = thm "iszero_def";
+
val number_of_succ = thm"number_of_succ";
val number_of_pred = thm"number_of_pred";
val number_of_minus = thm"number_of_minus";
@@ -86,7 +74,6 @@
val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
-val NCons_simps = thms"NCons_simps";
val bin_arith_extra_simps = thms"bin_arith_extra_simps";
val bin_arith_simps = thms"bin_arith_simps";
val bin_rel_simps = thms"bin_rel_simps";
@@ -298,10 +285,9 @@
bin_simps \\ [add_number_of_left, number_of_add RS sym];
(*To evaluate binary negations of coefficients*)
-val minus_simps = NCons_simps @
- [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
- bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
- bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
+ bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
(*To let us treat subtraction as addition*)
val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
@@ -335,10 +321,10 @@
val find_first_coeff = find_first_coeff []
val trans_tac = trans_tac
val norm_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
+ ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
diff_simps@minus_simps@add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
+ THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
+ THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
add_ac@mult_ac))
val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
@@ -411,10 +397,10 @@
val prove_conv = Bin_Simprocs.prove_conv_nohyps
val trans_tac = trans_tac
val norm_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
+ ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
diff_simps@minus_simps@add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
+ THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
+ THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
add_ac@mult_ac))
val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps add_0s@bin_simps))
--- a/src/HOL/Integ/presburger.ML Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/presburger.ML Thu Jul 01 12:29:53 2004 +0200
@@ -120,9 +120,9 @@
("HOL.max", nT --> nT --> nT),
("HOL.min", nT --> nT --> nT),
- ("Numeral.bin.Bit", binT --> bT --> binT),
- ("Numeral.bin.Pls", binT),
- ("Numeral.bin.Min", binT),
+ ("Numeral.Bit", binT --> bT --> binT),
+ ("Numeral.Pls", binT),
+ ("Numeral.Min", binT),
("Numeral.number_of", binT --> iT),
("Numeral.number_of", binT --> nT),
("0", nT),
--- a/src/HOL/IsaMakefile Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 01 12:29:53 2004 +0200
@@ -84,14 +84,14 @@
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
Fun.thy Gfp.ML Gfp.thy Hilbert_Choice.thy HOL.ML \
- HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Bin.thy \
+ HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
Integ/cooper_dec.ML Integ/cooper_proof.ML \
Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
- Nat.thy NatArith.ML NatArith.thy Numeral.thy \
+ Nat.thy NatArith.ML NatArith.thy \
Power.thy PreList.thy Product_Type.ML Product_Type.thy \
Refute.thy ROOT.ML \
Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
--- a/src/HOL/Library/Word.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Library/Word.thy Thu Jul 01 12:29:53 2004 +0200
@@ -378,13 +378,14 @@
constdefs
bv_to_nat :: "bit list => int"
- "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bv)"
+ "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bv)"
lemma [simp]: "bv_to_nat [] = 0"
by (simp add: bv_to_nat_def)
-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)"
- by (induct w,auto,simp add: iszero_def)
+lemma pos_number_of:
+ "number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
+by (simp add: mult_2)
lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
proof -
@@ -393,26 +394,24 @@
by (simp add: bv_to_nat'_def)
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)"
by (simp add: bv_to_nat'_def)
- 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"
+ 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"
proof (induct bs,simp add: bv_to_nat'_def,clarify)
fix x xs base
- 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"
+ 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"
assume base_pos: "(0::int) \<le> number_of base"
def qq == "number_of base::int"
- show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' bin.Pls (x # xs)"
+ show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' Numeral.Pls (x # xs)"
apply (unfold bv_to_nat'_def)
apply (simp only: foldl.simps)
apply (fold bv_to_nat'_def)
apply (subst ind [of "base BIT (x = \<one>)"])
using base_pos
apply simp
- apply (subst ind [of "bin.Pls BIT (x = \<one>)"])
+ apply (subst ind [of "Numeral.Pls BIT (x = \<one>)"])
apply simp
apply (subst pos_number_of [of "base" "x = \<one>"])
using base_pos
- apply simp
- apply (subst pos_number_of [of "bin.Pls" "x = \<one>"])
- apply simp
+ apply (subst pos_number_of [of "Numeral.Pls" "x = \<one>"])
apply (fold qq_def)
apply (simp add: ring_distrib)
done
@@ -2859,14 +2858,15 @@
lemmas [simp] = length_nat_non0
-lemma "nat_to_bv (number_of bin.Pls) = []"
+lemma "nat_to_bv (number_of Numeral.Pls) = []"
by simp
+(***NO LONGER WORKS
consts
fast_nat_to_bv_helper :: "bin => bit list => bit list"
primrec
- fast_nat_to_bv_Pls: "fast_nat_to_bv_helper bin.Pls res = res"
+ fast_nat_to_bv_Pls: "fast_nat_to_bv_helper Numeral.Pls res = res"
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)"
lemma fast_nat_to_bv_def:
@@ -2889,7 +2889,7 @@
by (simp add: qq_def)
with posbb
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)"
- apply (subst pos_number_of,simp)
+ apply (subst pos_number_of)
apply safe
apply (fold qq_def)
apply (cases "qq = 0")
@@ -2938,6 +2938,8 @@
declare fast_nat_to_bv_Bit [simp del]
declare fast_nat_to_bv_Bit0 [simp]
declare fast_nat_to_bv_Bit1 [simp]
+****)
+
consts
fast_bv_to_nat_helper :: "[bit list, bin] => bin"
@@ -2952,13 +2954,13 @@
lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)"
by simp
-lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs bin.Pls)"
+lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
proof (simp add: bv_to_nat_def)
have "\<forall> bin. (foldl (%bn b. bn BIT (b = \<one>)) bin bs) = (fast_bv_to_nat_helper bs bin)"
apply (induct bs,simp)
apply (case_tac a,simp_all)
done
- thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bs) == number_of (fast_bv_to_nat_helper bs bin.Pls)::int"
+ thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bs) == number_of (fast_bv_to_nat_helper bs Numeral.Pls)::int"
by simp
qed
@@ -2988,12 +2990,4 @@
lemma [code]: "bv_to_nat bs = list_rec (0::int) (\<lambda>b bs n. bitval b * 2 ^ length bs + n) bs"
by (induct bs,simp_all add: bv_to_nat_helper)
-text {* The following can be added for speedup, but depends on the
-exact definition of division and modulo of the ML compiler for soundness. *}
-
-(*
-consts_code "op div" ("'('(_') div '(_')')")
-consts_code "op mod" ("'('(_') mod '(_')')")
-*)
-
end
--- a/src/HOL/Library/word_setup.ML Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Library/word_setup.ML Thu Jul 01 12:29:53 2004 +0200
@@ -1,6 +1,8 @@
(* Title: HOL/Library/word_setup.ML
ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
+
+comments containing lcp are the removal of fast_bv_of_nat.
*)
local
@@ -10,9 +12,9 @@
fun is_const_bit (Const("Word.bit.Zero",_)) = true
| is_const_bit (Const("Word.bit.One",_)) = true
| is_const_bit _ = false
- fun num_is_usable (Const("Numeral.bin.Pls",_)) = true
- | num_is_usable (Const("Numeral.bin.Min",_)) = false
- | num_is_usable (Const("Numeral.bin.Bit",_) $ w $ b) =
+ fun num_is_usable (Const("Numeral.Pls",_)) = true
+ | num_is_usable (Const("Numeral.Min",_)) = false
+ | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
num_is_usable w andalso is_const_bool b
| num_is_usable _ = false
fun vec_is_usable (Const("List.list.Nil",_)) = true
@@ -21,22 +23,22 @@
| vec_is_usable _ = false
fun add_word thy =
let
- val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"
+ (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
val fast2_th = PureThy.get_thm thy "Word.fast_bv_to_nat_def"
- fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
+ (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
if num_is_usable t
then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
else None
- | f _ _ _ = None
+ | f _ _ _ = None **)
fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
if vec_is_usable t
then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
else None
| g _ _ _ = None
- val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f
+ (*lcp** val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
in
- Simplifier.change_simpset_of (op addsimprocs) [simproc1,simproc2] thy
+ Simplifier.change_simpset_of (op addsimprocs) [(*lcp*simproc1,**)simproc2] thy
end
in
val setup_word = [add_word]
--- a/src/HOL/Numeral.thy Wed Jun 30 14:04:58 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(* Title: HOL/Numeral.thy
- ID: $Id$
- Author: Larry Paulson and Markus Wenzel
-
-Generic numerals represented as twos-complement bit strings.
-*)
-
-theory Numeral = Datatype
-files "Tools/numeral_syntax.ML":
-
-text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
- Only qualified access bin.Pls and bin.Min is allowed.
- We do not hide Bit because we need the BIT infix syntax.*}
-
-text{*A number can have multiple representations, namely leading Falses with
-sign @{term Pls} and leading Trues with sign @{term Min}.
-See @{text "ZF/Integ/twos-compl.ML"}, function @{text int_of_binary},
-for the numerical interpretation.
-
-The representation expects that @{text "(m mod 2)"} is 0 or 1,
-even if m is negative;
-For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
-@{text "-5 = (-3)*2 + 1"}.
-*}
-
-datatype
- bin = Pls --{*Plus: Stands for an infinite string of leading Falses*}
- | Min --{*Minus: Stands for an infinite string of leading Trues*}
- | Bit bin bool (infixl "BIT" 90)
-
-axclass
- number < type -- {* for numeric types: nat, int, real, \dots *}
-
-consts
- number_of :: "bin => 'a::number"
-
-syntax
- "_Numeral" :: "num_const => 'a" ("_")
- Numeral0 :: 'a
- Numeral1 :: 'a
-
-translations
- "Numeral0" == "number_of bin.Pls"
- "Numeral1" == "number_of (bin.Pls BIT True)"
-
-
-setup NumeralSyntax.setup
-
-syntax (xsymbols)
- "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
-syntax (HTML output)
- "_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
-syntax (output)
- "_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
-translations
- "x\<twosuperior>" == "x^2"
- "x\<twosuperior>" <= "x^(2::nat)"
-
-
-lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
- -- {* Unfold all @{text let}s involving constants *}
- by (simp add: Let_def)
-
-lemma Let_0 [simp]: "Let 0 f == f 0"
- by (simp add: Let_def)
-
-lemma Let_1 [simp]: "Let 1 f == f 1"
- by (simp add: Let_def)
-
-
-consts
- NCons :: "[bin,bool]=>bin"
- bin_succ :: "bin=>bin"
- bin_pred :: "bin=>bin"
- bin_minus :: "bin=>bin"
- bin_add :: "[bin,bin]=>bin"
- bin_mult :: "[bin,bin]=>bin"
-
-text{*@{term NCons} inserts a bit, suppressing leading 0s and 1s*}
-primrec
- NCons_Pls: "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
- NCons_Min: "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
- NCons_BIT: "NCons (w BIT x) b = (w BIT x) BIT b"
-
-
-primrec
- bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True"
- bin_succ_Min: "bin_succ bin.Min = bin.Pls"
- bin_succ_BIT: "bin_succ(w BIT x) =
- (if x then bin_succ w BIT False
- else NCons w True)"
-
-primrec
- bin_pred_Pls: "bin_pred bin.Pls = bin.Min"
- bin_pred_Min: "bin_pred bin.Min = bin.Min BIT False"
- bin_pred_BIT: "bin_pred(w BIT x) =
- (if x then NCons w False
- else (bin_pred w) BIT True)"
-
-primrec
- bin_minus_Pls: "bin_minus bin.Pls = bin.Pls"
- bin_minus_Min: "bin_minus bin.Min = bin.Pls BIT True"
- bin_minus_BIT: "bin_minus(w BIT x) =
- (if x then bin_pred (NCons (bin_minus w) False)
- else bin_minus w BIT False)"
-
-primrec
- bin_add_Pls: "bin_add bin.Pls w = w"
- bin_add_Min: "bin_add bin.Min w = bin_pred w"
- bin_add_BIT:
- "bin_add (v BIT x) w =
- (case w of bin.Pls => v BIT x
- | bin.Min => bin_pred (v BIT x)
- | (w BIT y) =>
- NCons (bin_add v (if (x & y) then bin_succ w else w))
- (x~=y))"
-
-primrec
- bin_mult_Pls: "bin_mult bin.Pls w = bin.Pls"
- bin_mult_Min: "bin_mult bin.Min w = bin_minus w"
- bin_mult_BIT: "bin_mult (v BIT x) w =
- (if x then (bin_add (NCons (bin_mult v w) False) w)
- else (NCons (bin_mult v w) False))"
-
-
-subsection{*Extra rules for @{term bin_succ}, @{term bin_pred},
- @{term bin_add} and @{term bin_mult}*}
-
-lemma NCons_Pls_0: "NCons bin.Pls False = bin.Pls"
-by simp
-
-lemma NCons_Pls_1: "NCons bin.Pls True = bin.Pls BIT True"
-by simp
-
-lemma NCons_Min_0: "NCons bin.Min False = bin.Min BIT False"
-by simp
-
-lemma NCons_Min_1: "NCons bin.Min True = bin.Min"
-by simp
-
-lemma bin_succ_1: "bin_succ(w BIT True) = (bin_succ w) BIT False"
-by simp
-
-lemma bin_succ_0: "bin_succ(w BIT False) = NCons w True"
-by simp
-
-lemma bin_pred_1: "bin_pred(w BIT True) = NCons w False"
-by simp
-
-lemma bin_pred_0: "bin_pred(w BIT False) = (bin_pred w) BIT True"
-by simp
-
-lemma bin_minus_1: "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
-by simp
-
-lemma bin_minus_0: "bin_minus(w BIT False) = (bin_minus w) BIT False"
-by simp
-
-
-subsection{*Binary Addition and Multiplication:
- @{term bin_add} and @{term bin_mult}*}
-
-lemma bin_add_BIT_11:
- "bin_add (v BIT True) (w BIT True) =
- NCons (bin_add v (bin_succ w)) False"
-by simp
-
-lemma bin_add_BIT_10:
- "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
-by simp
-
-lemma bin_add_BIT_0:
- "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
-by auto
-
-lemma bin_add_Pls_right: "bin_add w bin.Pls = w"
-by (induct_tac "w", auto)
-
-lemma bin_add_Min_right: "bin_add w bin.Min = bin_pred w"
-by (induct_tac "w", auto)
-
-lemma bin_add_BIT_BIT:
- "bin_add (v BIT x) (w BIT y) =
- NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
-by simp
-
-lemma bin_mult_1:
- "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
-by simp
-
-lemma bin_mult_0: "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
-by simp
-
-
-end
--- a/src/HOL/Presburger.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Presburger.thy Thu Jul 01 12:29:53 2004 +0200
@@ -969,7 +969,7 @@
theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
by simp
-theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
+theorem number_of2: "(0::int) <= Numeral0" by simp
theorem Suc_plus1: "Suc n = n + 1" by simp
--- a/src/HOL/Real/PReal.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Real/PReal.thy Thu Jul 01 12:29:53 2004 +0200
@@ -705,7 +705,7 @@
from preal_nonempty [OF A]
show ?case by force
case (Suc k)
- from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" ..
+ from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
thus ?case by (force simp add: left_distrib add_ac prems)
qed
--- a/src/HOL/Real/Rational.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Real/Rational.thy Thu Jul 01 12:29:53 2004 +0200
@@ -674,25 +674,12 @@
instance rat :: number ..
-primrec -- {* the type constraint is essential! *}
- number_of_Pls: "number_of bin.Pls = 0"
- number_of_Min: "number_of bin.Min = - (1::rat)"
- number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
- number_of_Min [simp del]
- number_of_BIT [simp del]
+defs (overloaded)
+ rat_number_of_def: "(number_of w :: rat) == of_int (Rep_Bin w)"
+ --{*the type constraint is essential!*}
instance rat :: number_ring
-proof
- show "Numeral0 = (0::rat)" by (rule number_of_Pls)
- show "-1 = - (1::rat)" by (rule number_of_Min)
- fix w :: bin and x :: bool
- show "(number_of (w BIT x) :: rat) =
- (if x then 1 else 0) + number_of w + number_of w"
- by (rule number_of_BIT)
-qed
+by (intro_classes, simp add: rat_number_of_def)
declare diff_rat_def [symmetric]
--- a/src/HOL/Real/RealDef.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Real/RealDef.thy Thu Jul 01 12:29:53 2004 +0200
@@ -732,25 +732,12 @@
instance real :: number ..
-primrec (*the type constraint is essential!*)
- number_of_Pls: "number_of bin.Pls = 0"
- number_of_Min: "number_of bin.Min = - (1::real)"
- number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
- number_of_Min [simp del]
- number_of_BIT [simp del]
+defs (overloaded)
+ real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
+ --{*the type constraint is essential!*}
instance real :: number_ring
-proof
- show "Numeral0 = (0::real)" by (rule number_of_Pls)
- show "-1 = - (1::real)" by (rule number_of_Min)
- fix w :: bin and x :: bool
- show "(number_of (w BIT x) :: real) =
- (if x then 1 else 0) + number_of w + number_of w"
- by (rule number_of_BIT)
-qed
+by (intro_classes, simp add: real_number_of_def)
text{*Collapse applications of @{term real} to @{term number_of}*}
--- a/src/HOL/Tools/Presburger/presburger.ML Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Thu Jul 01 12:29:53 2004 +0200
@@ -120,9 +120,9 @@
("HOL.max", nT --> nT --> nT),
("HOL.min", nT --> nT --> nT),
- ("Numeral.bin.Bit", binT --> bT --> binT),
- ("Numeral.bin.Pls", binT),
- ("Numeral.bin.Min", binT),
+ ("Numeral.Bit", binT --> bT --> binT),
+ ("Numeral.Pls", binT),
+ ("Numeral.Min", binT),
("Numeral.number_of", binT --> iT),
("Numeral.number_of", binT --> nT),
("0", nT),
--- a/src/HOL/Tools/numeral_syntax.ML Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Thu Jul 01 12:29:53 2004 +0200
@@ -28,8 +28,8 @@
| prefix_len pred (x :: xs) =
if pred x then 1 + prefix_len pred xs else 0;
-fun bin_of (Const ("bin.Pls", _)) = []
- | bin_of (Const ("bin.Min", _)) = [~1]
+fun bin_of (Const ("Numeral.Pls", _)) = []
+ | bin_of (Const ("Numeral.Min", _)) = [~1]
| bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
@@ -70,7 +70,7 @@
(* theory setup *)
val setup =
- [Theory.hide_consts false ["Numeral.bin.Pls", "Numeral.bin.Min"],
+ [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
--- a/src/HOL/ex/BinEx.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/ex/BinEx.thy Thu Jul 01 12:29:53 2004 +0200
@@ -387,115 +387,7 @@
by simp
-subsection {* Normal form of bit strings *}
-
-text {*
- Definition of normal form for proving that binary arithmetic on
- normalized operands yields normalized results. Normal means no
- leading 0s on positive numbers and no leading 1s on negatives.
-*}
-
-consts normal :: "bin set"
-inductive normal
- intros
- Pls [simp]: "bin.Pls: normal"
- Min [simp]: "bin.Min: normal"
- BIT_F [simp]: "w: normal ==> w \<noteq> bin.Pls ==> w BIT False : normal"
- BIT_T [simp]: "w: normal ==> w \<noteq> bin.Min ==> w BIT True : normal"
-
-text {*
- \medskip Binary arithmetic on normalized operands yields normalized
- results.
-*}
-
-lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal"
- apply (case_tac c)
- apply auto
- done
-
-lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal"
- apply (erule normal.cases)
- apply auto
- done
-
-lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal"
- apply (induct w)
- apply (auto simp add: NCons_Pls NCons_Min)
- done
-
-lemma NCons_True: "NCons w True \<noteq> bin.Pls"
- apply (induct w)
- apply auto
- done
-
-lemma NCons_False: "NCons w False \<noteq> bin.Min"
- apply (induct w)
- apply auto
- done
-
-lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> normal"
- apply (erule normal.induct)
- apply (case_tac [4] w)
- apply (auto simp add: NCons_True bin_succ_BIT)
- done
-
-lemma bin_pred_normal [simp]: "w \<in> normal ==> bin_pred w \<in> normal"
- apply (erule normal.induct)
- apply (case_tac [3] w)
- apply (auto simp add: NCons_False bin_pred_BIT)
- done
-
-lemma bin_add_normal [rule_format]:
- "w \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> normal)"
- apply (induct w)
- apply simp
- apply simp
- apply (rule impI)
- apply (rule allI)
- apply (induct_tac z)
- apply (simp_all add: bin_add_BIT)
- apply (safe dest!: normal_BIT_D)
- apply simp_all
- done
-
-lemma normal_Pls_eq_0: "w \<in> normal ==> (w = bin.Pls) = (number_of w = (0::int))"
- apply (erule normal.induct)
- apply auto
- done
-
-lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"
- apply (erule normal.induct)
- apply (simp_all add: bin_minus_BIT)
- apply (rule normal.intros)
- apply assumption
- apply (simp add: normal_Pls_eq_0)
- apply (simp only: number_of_minus zminus_0 iszero_def
- minus_equation_iff [of _ "0"])
- done
-
-(*The previous command should have finished the proof but the lin-arith
-procedure at the end of simplificatioon fails.
-Problem: lin-arith correctly derives the contradictory thm
-"number_of w + 1 + - 0 \<le> 0 + number_of w" [..]
-which its local simplification setup should turn into False.
-But on the way we get
-
-Procedure "int_add_eval_numerals" produced rewrite rule:
-number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (bin.Pls BIT True))
-
-and eventually we arrive not at false but at
-
-"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (bin.Pls BIT True)))))"
-
-The simplification with eq_commute should now be obsolete.
-*)
-
-lemma bin_mult_normal [rule_format]:
- "w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"
- apply (erule normal.induct)
- apply (simp_all add: bin_minus_normal bin_mult_BIT)
- apply (safe dest!: normal_BIT_D)
- apply (simp add: bin_add_normal)
- done
+text{*The proofs about arithmetic yielding normal forms have been deleted:
+ they are irrelevant with the new treatment of numerals.*}
end
--- a/src/HOL/hologic.ML Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/hologic.ML Thu Jul 01 12:29:53 2004 +0200
@@ -282,9 +282,9 @@
val binT = Type ("Numeral.bin", []);
-val pls_const = Const ("Numeral.bin.Pls", binT)
-and min_const = Const ("Numeral.bin.Min", binT)
-and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
+val pls_const = Const ("Numeral.Pls", binT)
+and min_const = Const ("Numeral.Min", binT)
+and bit_const = Const ("Numeral.Bit", [binT, boolT] ---> binT);
fun number_of_const T = Const ("Numeral.number_of", binT --> T);
@@ -296,9 +296,9 @@
| dest_bit (Const ("True", _)) = 1
| dest_bit t = raise TERM("dest_bit", [t]);
-fun bin_of (Const ("Numeral.bin.Pls", _)) = []
- | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
- | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+fun bin_of (Const ("Numeral.Pls", _)) = []
+ | bin_of (Const ("Numeral.Min", _)) = [~1]
+ | bin_of (Const ("Numeral.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of t = raise TERM("bin_of", [t]);
val dest_binum = int_of o bin_of;