--- a/NEWS Tue Nov 19 01:30:14 2013 +0100
+++ b/NEWS Tue Nov 19 10:05:53 2013 +0100
@@ -18,6 +18,14 @@
even_zero_(nat|int) ~> even_zero
INCOMPATIBILITY.
+* Abolished neg_numeral.
+ * Canonical representation for minus one is "- 1".
+ * Canonical representation for other negative numbers is "- (numeral _)".
+ * When devising rules set for number calculation, consider the
+ following cases: 0, 1, numeral _, - 1, - numeral _.
+ * Syntax for negative numerals is mere input syntax.
+INCOMPATBILITY.
+
* Elimination of fact duplicates:
equals_zero_I ~> minus_unique
diff_eq_0_iff_eq ~> right_minus_eq
--- a/src/HOL/Archimedean_Field.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Archimedean_Field.thy Tue Nov 19 10:05:53 2013 +0100
@@ -204,8 +204,8 @@
lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
using floor_of_int [of "numeral v"] by simp
-lemma floor_neg_numeral [simp]: "floor (neg_numeral v) = neg_numeral v"
- using floor_of_int [of "neg_numeral v"] by simp
+lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v"
+ using floor_of_int [of "- numeral v"] by simp
lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
by (simp add: le_floor_iff)
@@ -218,7 +218,7 @@
by (simp add: le_floor_iff)
lemma neg_numeral_le_floor [simp]:
- "neg_numeral v \<le> floor x \<longleftrightarrow> neg_numeral v \<le> x"
+ "- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x"
by (simp add: le_floor_iff)
lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
@@ -232,7 +232,7 @@
by (simp add: less_floor_iff)
lemma neg_numeral_less_floor [simp]:
- "neg_numeral v < floor x \<longleftrightarrow> neg_numeral v + 1 \<le> x"
+ "- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x"
by (simp add: less_floor_iff)
lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
@@ -246,7 +246,7 @@
by (simp add: floor_le_iff)
lemma floor_le_neg_numeral [simp]:
- "floor x \<le> neg_numeral v \<longleftrightarrow> x < neg_numeral v + 1"
+ "floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
by (simp add: floor_le_iff)
lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
@@ -260,7 +260,7 @@
by (simp add: floor_less_iff)
lemma floor_less_neg_numeral [simp]:
- "floor x < neg_numeral v \<longleftrightarrow> x < neg_numeral v"
+ "floor x < - numeral v \<longleftrightarrow> x < - numeral v"
by (simp add: floor_less_iff)
text {* Addition and subtraction of integers *}
@@ -272,10 +272,6 @@
"floor (x + numeral v) = floor x + numeral v"
using floor_add_of_int [of x "numeral v"] by simp
-lemma floor_add_neg_numeral [simp]:
- "floor (x + neg_numeral v) = floor x + neg_numeral v"
- using floor_add_of_int [of x "neg_numeral v"] by simp
-
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
using floor_add_of_int [of x 1] by simp
@@ -286,10 +282,6 @@
"floor (x - numeral v) = floor x - numeral v"
using floor_diff_of_int [of x "numeral v"] by simp
-lemma floor_diff_neg_numeral [simp]:
- "floor (x - neg_numeral v) = floor x - neg_numeral v"
- using floor_diff_of_int [of x "neg_numeral v"] by simp
-
lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
using floor_diff_of_int [of x 1] by simp
@@ -353,8 +345,8 @@
lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
using ceiling_of_int [of "numeral v"] by simp
-lemma ceiling_neg_numeral [simp]: "ceiling (neg_numeral v) = neg_numeral v"
- using ceiling_of_int [of "neg_numeral v"] by simp
+lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v"
+ using ceiling_of_int [of "- numeral v"] by simp
lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
by (simp add: ceiling_le_iff)
@@ -367,7 +359,7 @@
by (simp add: ceiling_le_iff)
lemma ceiling_le_neg_numeral [simp]:
- "ceiling x \<le> neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v"
+ "ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
by (simp add: ceiling_le_iff)
lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
@@ -381,7 +373,7 @@
by (simp add: ceiling_less_iff)
lemma ceiling_less_neg_numeral [simp]:
- "ceiling x < neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v - 1"
+ "ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
by (simp add: ceiling_less_iff)
lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
@@ -395,7 +387,7 @@
by (simp add: le_ceiling_iff)
lemma neg_numeral_le_ceiling [simp]:
- "neg_numeral v \<le> ceiling x \<longleftrightarrow> neg_numeral v - 1 < x"
+ "- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x"
by (simp add: le_ceiling_iff)
lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
@@ -409,7 +401,7 @@
by (simp add: less_ceiling_iff)
lemma neg_numeral_less_ceiling [simp]:
- "neg_numeral v < ceiling x \<longleftrightarrow> neg_numeral v < x"
+ "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
by (simp add: less_ceiling_iff)
text {* Addition and subtraction of integers *}
@@ -421,10 +413,6 @@
"ceiling (x + numeral v) = ceiling x + numeral v"
using ceiling_add_of_int [of x "numeral v"] by simp
-lemma ceiling_add_neg_numeral [simp]:
- "ceiling (x + neg_numeral v) = ceiling x + neg_numeral v"
- using ceiling_add_of_int [of x "neg_numeral v"] by simp
-
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
using ceiling_add_of_int [of x 1] by simp
@@ -435,10 +423,6 @@
"ceiling (x - numeral v) = ceiling x - numeral v"
using ceiling_diff_of_int [of x "numeral v"] by simp
-lemma ceiling_diff_neg_numeral [simp]:
- "ceiling (x - neg_numeral v) = ceiling x - neg_numeral v"
- using ceiling_diff_of_int [of x "neg_numeral v"] by simp
-
lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
using ceiling_diff_of_int [of x 1] by simp
--- a/src/HOL/BNF/More_BNFs.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy Tue Nov 19 10:05:53 2013 +0100
@@ -973,8 +973,7 @@
using finite_Collect_mem .
ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
- by (metis (lifting, mono_tags) mem_Collect_eq rel_simps(54)
- setsum_gt_0_iff setsum_infinite)
+ by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
apply safe
apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
--- a/src/HOL/Code_Numeral.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Code_Numeral.thy Tue Nov 19 10:05:53 2013 +0100
@@ -96,10 +96,6 @@
qed
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
- by (unfold neg_numeral_def [abs_def]) transfer_prover
-
-lemma [transfer_rule]:
"fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
by (unfold Num.sub_def [abs_def]) transfer_prover
@@ -147,10 +143,6 @@
"int_of_integer (numeral k) = numeral k"
by transfer rule
-lemma int_of_integer_neg_numeral [simp]:
- "int_of_integer (neg_numeral k) = neg_numeral k"
- by transfer rule
-
lemma int_of_integer_sub [simp]:
"int_of_integer (Num.sub k l) = Num.sub k l"
by transfer rule
@@ -253,11 +245,11 @@
definition Neg :: "num \<Rightarrow> integer"
where
- [simp, code_abbrev]: "Neg = neg_numeral"
+ [simp, code_abbrev]: "Neg n = - Pos n"
lemma [transfer_rule]:
- "fun_rel HOL.eq pcr_integer neg_numeral Neg"
- by simp transfer_prover
+ "fun_rel HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
+ by (simp add: Neg_def [abs_def]) transfer_prover
code_datatype "0::integer" Pos Neg
@@ -272,7 +264,7 @@
"dup 0 = 0"
"dup (Pos n) = Pos (Num.Bit0 n)"
"dup (Neg n) = Neg (Num.Bit0 n)"
- by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
+ by (transfer, simp only: numeral_Bit0 minus_add_distrib)+
lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
is "\<lambda>m n. numeral m - numeral n :: int"
--- a/src/HOL/Complex.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Complex.thy Tue Nov 19 10:05:53 2013 +0100
@@ -108,7 +108,12 @@
definition complex_divide_def:
"x / (y\<Colon>complex) = x * inverse y"
-lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
+lemma Complex_eq_1 [simp]:
+ "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
+ by (simp add: complex_one_def)
+
+lemma Complex_eq_neg_1 [simp]:
+ "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
by (simp add: complex_one_def)
lemma complex_Re_one [simp]: "Re 1 = 1"
@@ -166,21 +171,21 @@
lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
using complex_Re_of_int [of "numeral v"] by simp
-lemma complex_Re_neg_numeral [simp]: "Re (neg_numeral v) = neg_numeral v"
- using complex_Re_of_int [of "neg_numeral v"] by simp
+lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v"
+ using complex_Re_of_int [of "- numeral v"] by simp
lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
using complex_Im_of_int [of "numeral v"] by simp
-lemma complex_Im_neg_numeral [simp]: "Im (neg_numeral v) = 0"
- using complex_Im_of_int [of "neg_numeral v"] by simp
+lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0"
+ using complex_Im_of_int [of "- numeral v"] by simp
lemma Complex_eq_numeral [simp]:
- "(Complex a b = numeral w) = (a = numeral w \<and> b = 0)"
+ "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
by (simp add: complex_eq_iff)
lemma Complex_eq_neg_numeral [simp]:
- "(Complex a b = neg_numeral w) = (a = neg_numeral w \<and> b = 0)"
+ "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
by (simp add: complex_eq_iff)
@@ -421,7 +426,7 @@
lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
by (simp add: complex_eq_iff)
-lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> neg_numeral w"
+lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
by (simp add: complex_eq_iff)
lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
@@ -508,7 +513,7 @@
lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"
by (simp add: complex_eq_iff)
-lemma complex_cnj_neg_numeral [simp]: "cnj (neg_numeral w) = neg_numeral w"
+lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
by (simp add: complex_eq_iff)
lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Nov 19 10:05:53 2013 +0100
@@ -11,8 +11,10 @@
"~~/src/HOL/Library/Code_Target_Numeral"
begin
-declare powr_numeral[simp]
-declare powr_neg_numeral[simp]
+declare powr_one [simp]
+declare powr_numeral [simp]
+declare powr_neg_one [simp]
+declare powr_neg_numeral [simp]
section "Horner Scheme"
@@ -1261,8 +1263,8 @@
unfolding cos_periodic_int ..
also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
- by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
- mult_minus_left mult_1_left) simp
+ by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
+ mult_minus_left mult_1_left) simp
also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
unfolding uminus_float.rep_eq cos_minus ..
also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1306,7 +1308,7 @@
also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
- minus_one[symmetric] mult_minus_left mult_1_left) simp
+ mult_minus_left mult_1_left) simp
also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
using lb_cos[OF lx_0 pi_lx] by simp
finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -2104,8 +2106,9 @@
lemma interpret_floatarith_num:
shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
and "interpret_floatarith (Num (Float 1 0)) vs = 1"
+ and "interpret_floatarith (Num (Float (- 1) 0)) vs = - 1"
and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a"
- and "interpret_floatarith (Num (Float (neg_numeral a) 0)) vs = neg_numeral a" by auto
+ and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a" by auto
subsection "Implement approximation function"
--- a/src/HOL/Decision_Procs/Cooper.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Tue Nov 19 10:05:53 2013 +0100
@@ -2006,9 +2006,10 @@
| SOME n => @{code Bound} (@{code nat_of_integer} n))
| num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0)
| num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
+ | num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1))
| num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) =
@{code C} (@{code int_of_integer} (HOLogic.dest_num t))
- | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t) =
+ | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} $ t) =
@{code C} (@{code int_of_integer} (~(HOLogic.dest_num t)))
| num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
| num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
--- a/src/HOL/Decision_Procs/MIR.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Tue Nov 19 10:05:53 2013 +0100
@@ -3154,7 +3154,7 @@
hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
by (simp only: algebra_simps)
hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
- by (simp add: algebra_simps minus_one [symmetric] del: minus_one)
+ by (simp add: algebra_simps)
with nob have ?case by blast }
ultimately show ?case by blast
next
@@ -5549,6 +5549,7 @@
| num_of_term vs @{term "real (1::int)"} = mk_C 1
| num_of_term vs @{term "0::real"} = mk_C 0
| num_of_term vs @{term "1::real"} = mk_C 1
+ | num_of_term vs @{term "- 1::real"} = mk_C (~ 1)
| num_of_term vs (Bound i) = mk_Bound i
| num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
| num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
@@ -5561,7 +5562,7 @@
| _ => error "num_of_term: unsupported Multiplication")
| num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
mk_C (HOLogic.dest_num t')
- | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t')) =
+ | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
mk_C (~ (HOLogic.dest_num t'))
| num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
@{code Floor} (num_of_term vs t')
@@ -5569,7 +5570,7 @@
@{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
| num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
mk_C (HOLogic.dest_num t')
- | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> real"} $ t') =
+ | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
mk_C (~ (HOLogic.dest_num t'))
| num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
@@ -5583,7 +5584,7 @@
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
| fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2)
- | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
+ | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2)
| fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Nov 19 10:05:53 2013 +0100
@@ -1256,12 +1256,10 @@
apply (case_tac n', simp, simp)
apply (case_tac n, simp, simp)
apply (case_tac n, case_tac n', simp add: Let_def)
- apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
- apply (auto simp add: polyadd_eq_const_degree)
+ apply (auto simp add: polyadd_eq_const_degree)[2]
apply (metis head_nz)
apply (metis head_nz)
apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
- apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
done
lemma polymul_head_polyeq:
--- a/src/HOL/Divides.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Divides.thy Tue Nov 19 10:05:53 2013 +0100
@@ -1919,10 +1919,9 @@
val zero = @{term "0 :: int"}
val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
- val simps = @{thms arith_simps} @ @{thms rel_simps} @
- map (fn th => th RS sym) [@{thm numeral_1_eq_1}]
- fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
- (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
+ val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
+ fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
+ (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
fun binary_proc proc ctxt ct =
(case Thm.term_of ct of
_ $ t $ u =>
@@ -1945,23 +1944,23 @@
simproc_setup binary_int_div
("numeral m div numeral n :: int" |
- "numeral m div neg_numeral n :: int" |
- "neg_numeral m div numeral n :: int" |
- "neg_numeral m div neg_numeral n :: int") =
+ "numeral m div - numeral n :: int" |
+ "- numeral m div numeral n :: int" |
+ "- numeral m div - numeral n :: int") =
{* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
simproc_setup binary_int_mod
("numeral m mod numeral n :: int" |
- "numeral m mod neg_numeral n :: int" |
- "neg_numeral m mod numeral n :: int" |
- "neg_numeral m mod neg_numeral n :: int") =
+ "numeral m mod - numeral n :: int" |
+ "- numeral m mod numeral n :: int" |
+ "- numeral m mod - numeral n :: int") =
{* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
lemmas posDivAlg_eqn_numeral [simp] =
posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
lemmas negDivAlg_eqn_numeral [simp] =
- negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w
+ negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
text{*Special-case simplification *}
@@ -1973,14 +1972,14 @@
div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
lemmas div_pos_neg_1_numeral [simp] =
- div_pos_neg [OF zero_less_one, of "neg_numeral w",
+ div_pos_neg [OF zero_less_one, of "- numeral w",
OF neg_numeral_less_zero] for w
lemmas mod_pos_pos_1_numeral [simp] =
mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
lemmas mod_pos_neg_1_numeral [simp] =
- mod_pos_neg [OF zero_less_one, of "neg_numeral w",
+ mod_pos_neg [OF zero_less_one, of "- numeral w",
OF neg_numeral_less_zero] for w
lemmas posDivAlg_eqn_1_numeral [simp] =
@@ -2290,6 +2289,8 @@
shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
using assms unfolding divmod_int_rel_def by auto
+declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}
+
lemma neg_divmod_int_rel_mult_2:
assumes "b \<le> 0"
assumes "divmod_int_rel (a + 1) b (q, r)"
@@ -2427,13 +2428,13 @@
lemma dvd_neg_numeral_left [simp]:
fixes y :: "'a::comm_ring_1"
- shows "(neg_numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
- unfolding neg_numeral_def minus_dvd_iff ..
+ shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
+ by (fact minus_dvd_iff)
lemma dvd_neg_numeral_right [simp]:
fixes x :: "'a::comm_ring_1"
- shows "x dvd (neg_numeral k) \<longleftrightarrow> x dvd (numeral k)"
- unfolding neg_numeral_def dvd_minus_iff ..
+ shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
+ by (fact dvd_minus_iff)
lemmas dvd_eq_mod_eq_0_numeral [simp] =
dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
--- a/src/HOL/GCD.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/GCD.thy Tue Nov 19 10:05:53 2013 +0100
@@ -134,6 +134,14 @@
lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
by (simp add: gcd_int_def)
+lemma gcd_neg_numeral_1_int [simp]:
+ "gcd (- numeral n :: int) x = gcd (numeral n) x"
+ by (fact gcd_neg1_int)
+
+lemma gcd_neg_numeral_2_int [simp]:
+ "gcd x (- numeral n :: int) = gcd x (numeral n)"
+ by (fact gcd_neg2_int)
+
lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
by(simp add: gcd_int_def)
--- a/src/HOL/IMP/Hoare_Examples.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/IMP/Hoare_Examples.thy Tue Nov 19 10:05:53 2013 +0100
@@ -2,17 +2,6 @@
theory Hoare_Examples imports Hoare begin
-text{* Improves proof automation for negative numerals: *}
-
-lemma add_neg1R[simp]:
- "x + -1 = x - (1 :: int)"
-by arith
-
-lemma add_neg_numeralR[simp]:
- "x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)"
-by (simp only: diff_minus_eq_add[symmetric] minus_neg_numeral)
-
-
text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
fun sum :: "int \<Rightarrow> int" where
--- a/src/HOL/Int.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Int.thy Tue Nov 19 10:05:53 2013 +0100
@@ -232,9 +232,8 @@
lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
-lemma of_int_neg_numeral [simp, code_post]: "of_int (neg_numeral k) = neg_numeral k"
- unfolding neg_numeral_def neg_numeral_class.neg_numeral_def
- by (simp only: of_int_minus of_int_numeral)
+lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
+ by simp
lemma of_int_power:
"of_int (z ^ n) = of_int z ^ n"
@@ -370,7 +369,7 @@
by (simp add: nat_eq_iff)
lemma nat_neg_numeral [simp]:
- "nat (neg_numeral k) = 0"
+ "nat (- numeral k) = 0"
by simp
lemma nat_2: "nat 2 = Suc (Suc 0)"
@@ -511,13 +510,13 @@
lemma nonneg_int_cases:
assumes "0 \<le> k" obtains n where "k = int n"
- using assms by (cases k, simp, simp del: of_nat_Suc)
+ using assms by (rule nonneg_eq_int)
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
-lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
+lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
@@ -525,15 +524,15 @@
lemmas max_number_of [simp] =
max_def [of "numeral u" "numeral v"]
- max_def [of "numeral u" "neg_numeral v"]
- max_def [of "neg_numeral u" "numeral v"]
- max_def [of "neg_numeral u" "neg_numeral v"] for u v
+ max_def [of "numeral u" "- numeral v"]
+ max_def [of "- numeral u" "numeral v"]
+ max_def [of "- numeral u" "- numeral v"] for u v
lemmas min_number_of [simp] =
min_def [of "numeral u" "numeral v"]
- min_def [of "numeral u" "neg_numeral v"]
- min_def [of "neg_numeral u" "numeral v"]
- min_def [of "neg_numeral u" "neg_numeral v"] for u v
+ min_def [of "numeral u" "- numeral v"]
+ min_def [of "- numeral u" "numeral v"]
+ min_def [of "- numeral u" "- numeral v"] for u v
subsubsection {* Binary comparisons *}
@@ -1070,8 +1069,6 @@
by auto
qed
-ML_val {* @{const_name neg_numeral} *}
-
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
by (insert abs_zmult_eq_1 [of m n], arith)
@@ -1127,62 +1124,30 @@
inverse_eq_divide [of "numeral w"] for w
lemmas inverse_eq_divide_neg_numeral [simp] =
- inverse_eq_divide [of "neg_numeral w"] for w
+ inverse_eq_divide [of "- numeral w"] for w
text {*These laws simplify inequalities, moving unary minus from a term
into the literal.*}
-lemmas le_minus_iff_numeral [simp, no_atp] =
- le_minus_iff [of "numeral v"]
- le_minus_iff [of "neg_numeral v"] for v
-
-lemmas equation_minus_iff_numeral [simp, no_atp] =
- equation_minus_iff [of "numeral v"]
- equation_minus_iff [of "neg_numeral v"] for v
+lemmas equation_minus_iff_numeral [no_atp] =
+ equation_minus_iff [of "numeral v"] for v
-lemmas minus_less_iff_numeral [simp, no_atp] =
- minus_less_iff [of _ "numeral v"]
- minus_less_iff [of _ "neg_numeral v"] for v
+lemmas minus_equation_iff_numeral [no_atp] =
+ minus_equation_iff [of _ "numeral v"] for v
-lemmas minus_le_iff_numeral [simp, no_atp] =
- minus_le_iff [of _ "numeral v"]
- minus_le_iff [of _ "neg_numeral v"] for v
-
-lemmas minus_equation_iff_numeral [simp, no_atp] =
- minus_equation_iff [of _ "numeral v"]
- minus_equation_iff [of _ "neg_numeral v"] for v
-
-text{*To Simplify Inequalities Where One Side is the Constant 1*}
+lemmas le_minus_iff_numeral [no_atp] =
+ le_minus_iff [of "numeral v"] for v
-lemma less_minus_iff_1 [simp]:
- fixes b::"'b::linordered_idom"
- shows "(1 < - b) = (b < -1)"
-by auto
-
-lemma le_minus_iff_1 [simp]:
- fixes b::"'b::linordered_idom"
- shows "(1 \<le> - b) = (b \<le> -1)"
-by auto
-
-lemma equation_minus_iff_1 [simp]:
- fixes b::"'b::ring_1"
- shows "(1 = - b) = (b = -1)"
-by (subst equation_minus_iff, auto)
+lemmas minus_le_iff_numeral [no_atp] =
+ minus_le_iff [of _ "numeral v"] for v
-lemma minus_less_iff_1 [simp]:
- fixes a::"'b::linordered_idom"
- shows "(- a < 1) = (-1 < a)"
-by auto
+lemmas less_minus_iff_numeral [no_atp] =
+ less_minus_iff [of "numeral v"] for v
-lemma minus_le_iff_1 [simp]:
- fixes a::"'b::linordered_idom"
- shows "(- a \<le> 1) = (-1 \<le> a)"
-by auto
+lemmas minus_less_iff_numeral [no_atp] =
+ minus_less_iff [of _ "numeral v"] for v
-lemma minus_equation_iff_1 [simp]:
- fixes a::"'b::ring_1"
- shows "(- a = 1) = (a = -1)"
-by (subst minus_equation_iff, auto)
+-- {* FIXME maybe simproc *}
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
@@ -1197,27 +1162,28 @@
lemmas le_divide_eq_numeral1 [simp] =
pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
- neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+ neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
lemmas divide_le_eq_numeral1 [simp] =
pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
- neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+ neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
lemmas less_divide_eq_numeral1 [simp] =
pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
- neg_less_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+ neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
lemmas divide_less_eq_numeral1 [simp] =
pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
- neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
+ neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
lemmas eq_divide_eq_numeral1 [simp] =
eq_divide_eq [of _ _ "numeral w"]
- eq_divide_eq [of _ _ "neg_numeral w"] for w
+ eq_divide_eq [of _ _ "- numeral w"] for w
lemmas divide_eq_eq_numeral1 [simp] =
divide_eq_eq [of _ "numeral w"]
- divide_eq_eq [of _ "neg_numeral w"] for w
+ divide_eq_eq [of _ "- numeral w"] for w
+
subsubsection{*Optional Simplification Rules Involving Constants*}
@@ -1225,27 +1191,27 @@
lemmas le_divide_eq_numeral =
le_divide_eq [of "numeral w"]
- le_divide_eq [of "neg_numeral w"] for w
+ le_divide_eq [of "- numeral w"] for w
lemmas divide_le_eq_numeral =
divide_le_eq [of _ _ "numeral w"]
- divide_le_eq [of _ _ "neg_numeral w"] for w
+ divide_le_eq [of _ _ "- numeral w"] for w
lemmas less_divide_eq_numeral =
less_divide_eq [of "numeral w"]
- less_divide_eq [of "neg_numeral w"] for w
+ less_divide_eq [of "- numeral w"] for w
lemmas divide_less_eq_numeral =
divide_less_eq [of _ _ "numeral w"]
- divide_less_eq [of _ _ "neg_numeral w"] for w
+ divide_less_eq [of _ _ "- numeral w"] for w
lemmas eq_divide_eq_numeral =
eq_divide_eq [of "numeral w"]
- eq_divide_eq [of "neg_numeral w"] for w
+ eq_divide_eq [of "- numeral w"] for w
lemmas divide_eq_eq_numeral =
divide_eq_eq [of _ _ "numeral w"]
- divide_eq_eq [of _ _ "neg_numeral w"] for w
+ divide_eq_eq [of _ _ "- numeral w"] for w
text{*Not good as automatic simprules because they cause case splits.*}
@@ -1257,21 +1223,20 @@
text{*Division By @{text "-1"}*}
lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
- unfolding minus_one [symmetric]
unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
by simp
lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
- unfolding minus_one [symmetric] by (rule divide_minus_left)
+ by (fact divide_minus_left)
lemma half_gt_zero_iff:
- "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
-by auto
+ "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
+ by auto
lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
- by simp
+ by (fact divide_numeral_1)
subsection {* The divides relation *}
@@ -1475,7 +1440,7 @@
[simp, code_abbrev]: "Pos = numeral"
definition Neg :: "num \<Rightarrow> int" where
- [simp, code_abbrev]: "Neg = neg_numeral"
+ [simp, code_abbrev]: "Neg n = - (Pos n)"
code_datatype "0::int" Pos Neg
@@ -1489,7 +1454,7 @@
"dup 0 = 0"
"dup (Pos n) = Pos (Num.Bit0 n)"
"dup (Neg n) = Neg (Num.Bit0 n)"
- unfolding Pos_def Neg_def neg_numeral_def
+ unfolding Pos_def Neg_def
by (simp_all add: numeral_Bit0)
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
@@ -1505,12 +1470,10 @@
"sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
"sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
"sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
- apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def
- neg_numeral_def numeral_BitM)
+ apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
apply (simp_all only: algebra_simps minus_diff_eq)
apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
apply (simp_all only: minus_add add.assoc left_minus)
- apply (simp_all only: algebra_simps right_minus)
done
text {* Implementations *}
@@ -1606,10 +1569,10 @@
"nat (Int.Neg k) = 0"
"nat 0 = 0"
"nat (Int.Pos k) = nat_of_num k"
- by (simp_all add: nat_of_num_numeral nat_numeral)
+ by (simp_all add: nat_of_num_numeral)
lemma (in ring_1) of_int_code [code]:
- "of_int (Int.Neg k) = neg_numeral k"
+ "of_int (Int.Neg k) = - numeral k"
"of_int 0 = 0"
"of_int (Int.Pos k) = numeral k"
by simp_all
@@ -1653,7 +1616,7 @@
lemma int_power:
"int (m ^ n) = int m ^ n"
- by (rule of_nat_power)
+ by (fact of_nat_power)
lemmas zpower_int = int_power [symmetric]
--- a/src/HOL/Library/Binomial.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Binomial.thy Tue Nov 19 10:05:53 2013 +0100
@@ -370,7 +370,7 @@
by auto
from False show ?thesis
by (simp add: pochhammer_def gbinomial_def field_simps
- eq setprod_timesf[symmetric] del: minus_one)
+ eq setprod_timesf[symmetric])
qed
lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n"
@@ -441,9 +441,9 @@
from eq[symmetric]
have ?thesis using kn
apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
- gbinomial_pochhammer field_simps pochhammer_Suc_setprod del: minus_one)
+ gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
- of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one)
+ of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
unfolding mult_assoc[symmetric]
unfolding setprod_timesf[symmetric]
--- a/src/HOL/Library/Bit.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Bit.thy Tue Nov 19 10:05:53 2013 +0100
@@ -147,11 +147,11 @@
text {* All numerals reduce to either 0 or 1. *}
-lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
- by (simp only: minus_one [symmetric] uminus_bit_def)
+lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
+ by (simp only: uminus_bit_def)
-lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
- by (simp only: neg_numeral_def uminus_bit_def)
+lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
+ by (simp only: uminus_bit_def)
lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
by (simp only: numeral_Bit0 bit_add_self)
--- a/src/HOL/Library/Code_Prolog.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Code_Prolog.thy Tue Nov 19 10:05:53 2013 +0100
@@ -12,10 +12,8 @@
section {* Setup for Numerals *}
-setup {* Predicate_Compile_Data.ignore_consts
- [@{const_name numeral}, @{const_name neg_numeral}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
-setup {* Predicate_Compile_Data.keep_functions
- [@{const_name numeral}, @{const_name neg_numeral}] *}
+setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
end
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Nov 19 10:05:53 2013 +0100
@@ -169,7 +169,7 @@
by simp
lemma [code_unfold del]:
- "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
+ "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
by simp
hide_const (open) real_of_int
--- a/src/HOL/Library/Code_Target_Int.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Tue Nov 19 10:05:53 2013 +0100
@@ -30,7 +30,7 @@
by transfer simp
lemma [code_abbrev]:
- "int_of_integer (neg_numeral k) = Int.Neg k"
+ "int_of_integer (- numeral k) = Int.Neg k"
by transfer simp
lemma [code, symmetric, code_post]:
--- a/src/HOL/Library/Extended.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Extended.thy Tue Nov 19 10:05:53 2013 +0100
@@ -161,8 +161,8 @@
apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
done
-lemma Fin_neg_numeral: "Fin(neg_numeral w) = - numeral w"
-by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric])
+lemma Fin_neg_numeral: "Fin (- numeral w) = - numeral w"
+by (simp only: Fin_numeral uminus_extended.simps[symmetric])
instantiation extended :: (lattice)bounded_lattice
--- a/src/HOL/Library/Float.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Float.thy Tue Nov 19 10:05:53 2013 +0100
@@ -45,7 +45,7 @@
lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
-lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
+lemma neg_numeral_float[simp]: "- numeral i \<in> float" by (intro floatI[of "- numeral i" 0]) simp
lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp
@@ -53,7 +53,7 @@
lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp
lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \<in> float" by (intro floatI[of 1 "-i"]) simp
lemma two_powr_numeral_float[simp]: "2 powr numeral i \<in> float" by (intro floatI[of 1 "numeral i"]) simp
-lemma two_powr_neg_numeral_float[simp]: "2 powr neg_numeral i \<in> float" by (intro floatI[of 1 "neg_numeral i"]) simp
+lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \<in> float" by (intro floatI[of 1 "- numeral i"]) simp
lemma two_pow_float[simp]: "2 ^ n \<in> float" by (intro floatI[of 1 "n"]) (simp add: powr_realpow)
lemma real_of_float_float[simp]: "real (f::float) \<in> float" by (cases f) simp
@@ -121,11 +121,11 @@
qed
lemma div_neg_numeral_Bit0_float[simp]:
- assumes x: "x / numeral n \<in> float" shows "x / (neg_numeral (Num.Bit0 n)) \<in> float"
+ assumes x: "x / numeral n \<in> float" shows "x / (- numeral (Num.Bit0 n)) \<in> float"
proof -
have "- (x / numeral (Num.Bit0 n)) \<in> float" using x by simp
- also have "- (x / numeral (Num.Bit0 n)) = x / neg_numeral (Num.Bit0 n)"
- unfolding neg_numeral_def by (simp del: minus_numeral)
+ also have "- (x / numeral (Num.Bit0 n)) = x / - numeral (Num.Bit0 n)"
+ by simp
finally show ?thesis .
qed
@@ -197,7 +197,7 @@
then show "\<exists>c. a < c \<and> c < b"
apply (intro exI[of _ "(a + b) * Float 1 -1"])
apply transfer
- apply (simp add: powr_neg_numeral)
+ apply (simp add: powr_minus)
done
qed
@@ -226,16 +226,16 @@
"fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
-lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
- by (simp add: minus_numeral[symmetric] del: minus_numeral)
+lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
+ by simp
lemma transfer_neg_numeral [transfer_rule]:
- "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
+ "fun_rel (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
lemma
shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
- and float_of_neg_numeral[simp]: "neg_numeral k = float_of (neg_numeral k)"
+ and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
unfolding real_of_float_eq by simp_all
subsection {* Represent floats as unique mantissa and exponent *}
@@ -439,7 +439,7 @@
by transfer simp
hide_fact (open) compute_float_numeral
-lemma compute_float_neg_numeral[code_abbrev]: "Float (neg_numeral k) 0 = neg_numeral k"
+lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k"
by transfer simp
hide_fact (open) compute_float_neg_numeral
@@ -960,7 +960,7 @@
also have "... < (1 / 2) * 2 powr real (rat_precision n (int x) (int y))"
apply (rule mult_strict_right_mono) by (insert assms) auto
also have "\<dots> = 2 powr real (rat_precision n (int x) (int y) - 1)"
- using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_neg_numeral)
+ using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_minus)
also have "\<dots> = 2 ^ nat (rat_precision n (int x) (int y) - 1)"
using rat_precision_pos[of x y n] assms by (simp add: powr_realpow[symmetric])
also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Nov 19 10:05:53 2013 +0100
@@ -384,8 +384,8 @@
by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
fps_const_add [symmetric])
-lemma neg_numeral_fps_const: "neg_numeral k = fps_const (neg_numeral k)"
- by (simp only: neg_numeral_def numeral_fps_const fps_const_neg)
+lemma neg_numeral_fps_const: "- numeral k = fps_const (- numeral k)"
+ by (simp only: numeral_fps_const fps_const_neg)
subsection{* The eXtractor series X*}
@@ -1202,7 +1202,7 @@
have eq: "(1 + X) * ?r = 1"
unfolding minus_one_power_iff
by (auto simp add: field_simps fps_eq_iff)
- show ?thesis by (auto simp add: eq intro: fps_inverse_unique simp del: minus_one)
+ show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
qed
@@ -1245,7 +1245,7 @@
lemma numeral_compose[simp]: "(numeral k::('a::{comm_ring_1}) fps) oo b = numeral k"
unfolding numeral_fps_const by simp
-lemma neg_numeral_compose[simp]: "(neg_numeral k::('a::{comm_ring_1}) fps) oo b = neg_numeral k"
+lemma neg_numeral_compose[simp]: "(- numeral k::('a::{comm_ring_1}) fps) oo b = - numeral k"
unfolding neg_numeral_fps_const by simp
lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)"
@@ -2363,7 +2363,7 @@
next
case (Suc n1)
have "?i $ n = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1"
- by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
+ by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} +
(X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
using a0 a1 Suc by (simp add: fps_inv_def)
@@ -2404,7 +2404,7 @@
next
case (Suc n1)
have "?i $ n = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + fps_ginv b a $ Suc n1 * (a $ 1)^ Suc n1"
- by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
+ by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} +
(b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})"
using a0 a1 Suc by (simp add: fps_ginv_def)
@@ -2564,9 +2564,9 @@
lemma fps_compose_mult_distrib:
- assumes c0: "c$0 = (0::'a::idom)"
- shows "(a * b) oo c = (a oo c) * (b oo c)" (is "?l = ?r")
- apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma[OF c0])
+ assumes c0: "c $ 0 = (0::'a::idom)"
+ shows "(a * b) oo c = (a oo c) * (b oo c)"
+ apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma [OF c0])
apply (simp add: fps_compose_nth fps_mult_nth setsum_left_distrib)
done
@@ -2941,7 +2941,7 @@
(is "inverse ?l = ?r")
proof -
have th: "?l * ?r = 1"
- by (auto simp add: field_simps fps_eq_iff minus_one_power_iff simp del: minus_one)
+ by (auto simp add: field_simps fps_eq_iff minus_one_power_iff)
have th': "?l $ 0 \<noteq> 0" by (simp add: )
from fps_inverse_unique[OF th' th] show ?thesis .
qed
@@ -3165,7 +3165,7 @@
have th: "?r$0 \<noteq> 0" by simp
have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
by (simp add: fps_inverse_deriv[OF th] fps_divide_def
- power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg minus_one)
+ power2_eq_square mult_commute fps_const_neg[symmetric] del: fps_const_neg)
have eq: "inverse ?r $ 0 = 1"
by (simp add: fps_inverse_def)
from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
@@ -3276,7 +3276,7 @@
have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
unfolding m1nk
unfolding m h pochhammer_Suc_setprod
- apply (simp add: field_simps del: fact_Suc minus_one)
+ apply (simp add: field_simps del: fact_Suc)
unfolding fact_altdef_nat id_def
unfolding of_nat_setprod
unfolding setprod_timesf[symmetric]
@@ -3593,7 +3593,7 @@
unfolding even_mult_two_ex by blast
have "?l $n = ?r$n"
- by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus)
+ by (simp add: m fps_sin_def fps_cos_def power_mult_distrib power_mult power_minus [of "c ^ 2"])
}
moreover
{
@@ -3602,7 +3602,7 @@
unfolding odd_nat_equiv_def2 by (auto simp add: mult_2)
have "?l $n = ?r$n"
by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
- power_mult power_minus)
+ power_mult power_minus [of "c ^ 2"])
}
ultimately have "?l $n = ?r$n" by blast
} then show ?thesis by (simp add: fps_eq_iff)
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Nov 19 10:05:53 2013 +0100
@@ -207,12 +207,14 @@
from unimodular_reduce_norm[OF th0] o
have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
- apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp del: minus_one add: minus_one [symmetric])
+ apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp)
apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
apply (rule_tac x="- ii" in exI, simp add: m power_mult)
apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
- apply (rule_tac x="ii" in exI, simp add: m power_mult)
+ apply (auto simp add: m power_mult)
+ apply (rule_tac x="ii" in exI)
+ apply (auto simp add: m power_mult)
done
then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
let ?w = "v / complex_of_real (root n (cmod b))"
--- a/src/HOL/Library/Polynomial.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Polynomial.thy Tue Nov 19 10:05:53 2013 +0100
@@ -1575,12 +1575,12 @@
lemma poly_div_minus_left [simp]:
fixes x y :: "'a::field poly"
shows "(- x) div y = - (x div y)"
- using div_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
+ using div_smult_left [of "- 1::'a"] by simp
lemma poly_mod_minus_left [simp]:
fixes x y :: "'a::field poly"
shows "(- x) mod y = - (x mod y)"
- using mod_smult_left [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
+ using mod_smult_left [of "- 1::'a"] by simp
lemma pdivmod_rel_smult_right:
"\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
@@ -1597,13 +1597,12 @@
lemma poly_div_minus_right [simp]:
fixes x y :: "'a::field poly"
shows "x div (- y) = - (x div y)"
- using div_smult_right [of "- 1::'a"]
- by (simp add: nonzero_inverse_minus_eq del: minus_one) (* FIXME *)
+ using div_smult_right [of "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
lemma poly_mod_minus_right [simp]:
fixes x y :: "'a::field poly"
shows "x mod (- y) = x mod y"
- using mod_smult_right [of "- 1::'a"] by (simp del: minus_one) (* FIXME *)
+ using mod_smult_right [of "- 1::'a"] by simp
lemma pdivmod_rel_mult:
"\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Nov 19 10:05:53 2013 +0100
@@ -45,8 +45,8 @@
section {* Setup for Numerals *}
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}
-setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}, @{const_name neg_numeral}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}] *}
+setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}] *}
setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue Nov 19 10:05:53 2013 +0100
@@ -875,7 +875,6 @@
@{term "0::real"}, @{term "1::real"},
@{term "numeral :: num => nat"},
@{term "numeral :: num => real"},
- @{term "neg_numeral :: num => real"},
@{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}];
fun check_sos kcts ct =
--- a/src/HOL/List.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/List.thy Tue Nov 19 10:05:53 2013 +0100
@@ -3072,9 +3072,9 @@
lemmas upto_rec_numeral [simp] =
upto.simps[of "numeral m" "numeral n"]
- upto.simps[of "numeral m" "neg_numeral n"]
- upto.simps[of "neg_numeral m" "numeral n"]
- upto.simps[of "neg_numeral m" "neg_numeral n"] for m n
+ upto.simps[of "numeral m" "- numeral n"]
+ upto.simps[of "- numeral m" "numeral n"]
+ upto.simps[of "- numeral m" "- numeral n"] for m n
lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
by(simp add: upto.simps)
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Tue Nov 19 10:05:53 2013 +0100
@@ -79,8 +79,8 @@
lemma real_is_int_numeral[simp]: "real_is_int (numeral x)"
by (auto simp: real_is_int_def intro!: exI[of _ "numeral x"])
-lemma real_is_int_neg_numeral[simp]: "real_is_int (neg_numeral x)"
- by (auto simp: real_is_int_def intro!: exI[of _ "neg_numeral x"])
+lemma real_is_int_neg_numeral[simp]: "real_is_int (- numeral x)"
+ by (auto simp: real_is_int_def intro!: exI[of _ "- numeral x"])
lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
by (simp add: int_of_real_def)
@@ -96,7 +96,7 @@
by (intro some_equality)
(auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
-lemma int_of_real_neg_numeral[simp]: "int_of_real (neg_numeral b) = neg_numeral b"
+lemma int_of_real_neg_numeral[simp]: "int_of_real (- numeral b) = - numeral b"
unfolding int_of_real_def
by (intro some_equality)
(auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Nov 19 10:05:53 2013 +0100
@@ -228,7 +228,10 @@
then show ?case by vector
qed
-lemma one_index[simp]: "(1 :: 'a::one ^'n)$i = 1"
+lemma one_index [simp]: "(1 :: 'a :: one ^ 'n) $ i = 1"
+ by vector
+
+lemma neg_one_index [simp]: "(- 1 :: 'a :: {one, uminus} ^ 'n) $ i = - 1"
by vector
instance vec :: (semiring_char_0, finite) semiring_char_0
@@ -244,8 +247,8 @@
lemma numeral_index [simp]: "numeral w $ i = numeral w"
by (induct w) (simp_all only: numeral.simps vector_add_component one_index)
-lemma neg_numeral_index [simp]: "neg_numeral w $ i = neg_numeral w"
- by (simp only: neg_numeral_def vector_uminus_component numeral_index)
+lemma neg_numeral_index [simp]: "- numeral w $ i = - numeral w"
+ by (simp only: vector_uminus_component numeral_index)
instance vec :: (comm_ring_1, finite) comm_ring_1 ..
instance vec :: (ring_char_0, finite) ring_char_0 ..
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Nov 19 10:05:53 2013 +0100
@@ -337,10 +337,10 @@
by (simp add: bilinear_def linear_iff)
lemma bilinear_lneg: "bilinear h \<Longrightarrow> h (- x) y = - h x y"
- by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul)
+ by (drule bilinear_lmul [of _ "- 1"]) simp
lemma bilinear_rneg: "bilinear h \<Longrightarrow> h x (- y) = - h x y"
- by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul)
+ by (drule bilinear_rmul [of _ _ "- 1"]) simp
lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
using add_imp_eq[of x y 0] by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 19 10:05:53 2013 +0100
@@ -5163,9 +5163,8 @@
lemma open_negations:
fixes s :: "'a::real_normed_vector set"
- shows "open s \<Longrightarrow> open ((\<lambda> x. -x) ` s)"
- unfolding scaleR_minus1_left [symmetric]
- by (rule open_scaling, auto)
+ shows "open s \<Longrightarrow> open ((\<lambda>x. - x) ` s)"
+ using open_scaling [of "- 1" s] by simp
lemma open_translation:
fixes s :: "'a::real_normed_vector set"
--- a/src/HOL/NSA/HTranscendental.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Tue Nov 19 10:05:53 2013 +0100
@@ -258,7 +258,7 @@
simp add: mult_assoc)
apply (rule approx_add_right_cancel [where d="-1"])
apply (rule approx_sym [THEN [2] approx_trans2])
-apply (auto simp add: mem_infmal_iff minus_one [symmetric] simp del: minus_one)
+apply (auto simp add: mem_infmal_iff)
done
lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
@@ -450,7 +450,7 @@
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
simp add: mult_assoc)
apply (rule approx_add_right_cancel [where d = "-1"])
-apply (simp add: minus_one [symmetric] del: minus_one)
+apply simp
done
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
--- a/src/HOL/NSA/HyperDef.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/HyperDef.thy Tue Nov 19 10:05:53 2013 +0100
@@ -425,7 +425,7 @@
declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w
lemma power_hypreal_of_real_neg_numeral:
- "(neg_numeral v :: hypreal) ^ n = hypreal_of_real ((neg_numeral v) ^ n)"
+ "(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)"
by simp
declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w
(*
--- a/src/HOL/NSA/NSA.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/NSA.thy Tue Nov 19 10:05:53 2013 +0100
@@ -654,7 +654,7 @@
(*reorientation simplification procedure: reorients (polymorphic)
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
simproc_setup approx_reorient_simproc
- ("0 @= x" | "1 @= y" | "numeral w @= z" | "neg_numeral w @= r") =
+ ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") =
{*
let val rule = @{thm approx_reorient} RS eq_reflection
fun proc phi ss ct = case term_of ct of
@@ -1849,8 +1849,12 @@
lemma st_numeral [simp]: "st (numeral w) = numeral w"
by (rule Reals_numeral [THEN st_SReal_eq])
-lemma st_neg_numeral [simp]: "st (neg_numeral w) = neg_numeral w"
-by (rule Reals_neg_numeral [THEN st_SReal_eq])
+lemma st_neg_numeral [simp]: "st (- numeral w) = - numeral w"
+proof -
+ from Reals_numeral have "numeral w \<in> \<real>" .
+ then have "- numeral w \<in> \<real>" by simp
+ with st_SReal_eq show ?thesis .
+qed
lemma st_0 [simp]: "st 0 = 0"
by (simp add: st_SReal_eq)
@@ -1858,6 +1862,9 @@
lemma st_1 [simp]: "st 1 = 1"
by (simp add: st_SReal_eq)
+lemma st_neg_1 [simp]: "st (- 1) = - 1"
+by (simp add: st_SReal_eq)
+
lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x"
by (simp add: st_unique st_SReal st_approx_self approx_minus)
--- a/src/HOL/NSA/NSComplex.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/NSComplex.thy Tue Nov 19 10:05:53 2013 +0100
@@ -635,7 +635,7 @@
by transfer (rule of_real_numeral [symmetric])
lemma hcomplex_hypreal_neg_numeral:
- "hcomplex_of_complex (neg_numeral w) = hcomplex_of_hypreal(neg_numeral w)"
+ "hcomplex_of_complex (- numeral w) = hcomplex_of_hypreal(- numeral w)"
by transfer (rule of_real_neg_numeral [symmetric])
lemma hcomplex_numeral_hcnj [simp]:
@@ -647,7 +647,7 @@
by transfer (rule norm_numeral)
lemma hcomplex_neg_numeral_hcmod [simp]:
- "hcmod(neg_numeral v :: hcomplex) = (numeral v :: hypreal)"
+ "hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)"
by transfer (rule norm_neg_numeral)
lemma hcomplex_numeral_hRe [simp]:
--- a/src/HOL/NSA/StarDef.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/NSA/StarDef.thy Tue Nov 19 10:05:53 2013 +0100
@@ -968,13 +968,13 @@
by transfer (rule refl)
lemma star_neg_numeral_def [transfer_unfold]:
- "neg_numeral k = star_of (neg_numeral k)"
-by (simp only: neg_numeral_def star_of_minus star_of_numeral)
+ "- numeral k = star_of (- numeral k)"
+by (simp only: star_of_minus star_of_numeral)
-lemma Standard_neg_numeral [simp]: "neg_numeral k \<in> Standard"
-by (simp add: star_neg_numeral_def)
+lemma Standard_neg_numeral [simp]: "- numeral k \<in> Standard"
+ using star_neg_numeral_def [of k] by simp
-lemma star_of_neg_numeral [simp]: "star_of (neg_numeral k) = neg_numeral k"
+lemma star_of_neg_numeral [simp]: "star_of (- numeral k) = - numeral k"
by transfer (rule refl)
lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
@@ -987,12 +987,12 @@
star_of_less [of _ "numeral k", simplified star_of_numeral]
star_of_le [of _ "numeral k", simplified star_of_numeral]
star_of_eq [of _ "numeral k", simplified star_of_numeral]
- star_of_less [of "neg_numeral k", simplified star_of_numeral]
- star_of_le [of "neg_numeral k", simplified star_of_numeral]
- star_of_eq [of "neg_numeral k", simplified star_of_numeral]
- star_of_less [of _ "neg_numeral k", simplified star_of_numeral]
- star_of_le [of _ "neg_numeral k", simplified star_of_numeral]
- star_of_eq [of _ "neg_numeral k", simplified star_of_numeral] for k
+ star_of_less [of "- numeral k", simplified star_of_numeral]
+ star_of_le [of "- numeral k", simplified star_of_numeral]
+ star_of_eq [of "- numeral k", simplified star_of_numeral]
+ star_of_less [of _ "- numeral k", simplified star_of_numeral]
+ star_of_le [of _ "- numeral k", simplified star_of_numeral]
+ star_of_eq [of _ "- numeral k", simplified star_of_numeral] for k
lemma Standard_of_nat [simp]: "of_nat n \<in> Standard"
by (simp add: star_of_nat_def)
--- a/src/HOL/Nominal/Nominal.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Nominal/Nominal.thy Tue Nov 19 10:05:53 2013 +0100
@@ -3517,7 +3517,7 @@
by (simp add: perm_int_def perm_int_def)
lemma neg_numeral_int_eqvt:
- shows "pi\<bullet>((neg_numeral n)::int) = neg_numeral n"
+ shows "pi\<bullet>((- numeral n)::int) = - numeral n"
by (simp add: perm_int_def perm_int_def)
lemma max_int_eqvt:
--- a/src/HOL/Num.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Num.thy Tue Nov 19 10:05:53 2013 +0100
@@ -275,16 +275,6 @@
end
-text {* Negative numerals. *}
-
-class neg_numeral = numeral + group_add
-begin
-
-definition neg_numeral :: "num \<Rightarrow> 'a" where
- "neg_numeral k = - numeral k"
-
-end
-
text {* Numeral syntax. *}
syntax
@@ -299,8 +289,8 @@
| (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
| (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
else raise Match
- val pos = Syntax.const @{const_name numeral}
- val neg = Syntax.const @{const_name neg_numeral}
+ val numeral = Syntax.const @{const_name numeral}
+ val uminus = Syntax.const @{const_name uminus}
val one = Syntax.const @{const_name Groups.one}
val zero = Syntax.const @{const_name Groups.zero}
fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
@@ -311,8 +301,9 @@
in
if value = 0 then zero else
if value > 0
- then pos $ num_of_int value
- else neg $ num_of_int (~value)
+ then numeral $ num_of_int value
+ else if value = ~1 then uminus $ one
+ else uminus $ (numeral $ num_of_int (~value))
end
| numeral_tr ts = raise TERM ("numeral_tr", ts);
in [("_Numeral", K numeral_tr)] end
@@ -323,12 +314,12 @@
fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
| dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
| dest_num (Const (@{const_syntax One}, _)) = 1;
- fun num_tr' sign ctxt T [n] =
+ fun num_tr' ctxt T [n] =
let
val k = dest_num n;
val t' =
Syntax.const @{syntax_const "_Numeral"} $
- Syntax.free (sign ^ string_of_int k);
+ Syntax.free (string_of_int k);
in
(case T of
Type (@{type_name fun}, [_, T']) =>
@@ -339,8 +330,7 @@
| _ => if T = dummyT then t' else raise Match)
end;
in
- [(@{const_syntax numeral}, num_tr' ""),
- (@{const_syntax neg_numeral}, num_tr' "-")]
+ [(@{const_syntax numeral}, num_tr')]
end
*}
@@ -383,9 +373,13 @@
Structures with negation: class @{text neg_numeral}
*}
-context neg_numeral
+class neg_numeral = numeral + group_add
begin
+lemma uminus_numeral_One:
+ "- Numeral1 = - 1"
+ by (simp add: numeral_One)
+
text {* Numerals form an abelian subgroup. *}
inductive is_num :: "'a \<Rightarrow> bool" where
@@ -403,7 +397,7 @@
apply simp
apply (rule_tac a=x in add_left_imp_eq)
apply (rule_tac a=x in add_right_imp_eq)
- apply (simp add: add_assoc minus_add_cancel)
+ apply (simp add: add_assoc)
apply (simp add: add_assoc [symmetric], simp add: add_assoc)
apply (rule_tac a=x in add_left_imp_eq)
apply (rule_tac a=x in add_right_imp_eq)
@@ -431,77 +425,85 @@
by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq)
lemma dbl_simps [simp]:
- "dbl (neg_numeral k) = neg_numeral (Bit0 k)"
+ "dbl (- numeral k) = - dbl (numeral k)"
"dbl 0 = 0"
"dbl 1 = 2"
+ "dbl (- 1) = - 2"
"dbl (numeral k) = numeral (Bit0 k)"
- by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
+ by (simp_all add: dbl_def numeral.simps minus_add)
lemma dbl_inc_simps [simp]:
- "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
+ "dbl_inc (- numeral k) = - dbl_dec (numeral k)"
"dbl_inc 0 = 1"
"dbl_inc 1 = 3"
+ "dbl_inc (- 1) = - 1"
"dbl_inc (numeral k) = numeral (Bit1 k)"
- by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
+ by (simp_all add: dbl_inc_def dbl_dec_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
lemma dbl_dec_simps [simp]:
- "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
- "dbl_dec 0 = -1"
+ "dbl_dec (- numeral k) = - dbl_inc (numeral k)"
+ "dbl_dec 0 = - 1"
"dbl_dec 1 = 1"
+ "dbl_dec (- 1) = - 3"
"dbl_dec (numeral k) = numeral (BitM k)"
- by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
+ by (simp_all add: dbl_dec_def dbl_inc_def numeral.simps numeral_BitM is_num_normalize)
lemma sub_num_simps [simp]:
"sub One One = 0"
- "sub One (Bit0 l) = neg_numeral (BitM l)"
- "sub One (Bit1 l) = neg_numeral (Bit0 l)"
+ "sub One (Bit0 l) = - numeral (BitM l)"
+ "sub One (Bit1 l) = - numeral (Bit0 l)"
"sub (Bit0 k) One = numeral (BitM k)"
"sub (Bit1 k) One = numeral (Bit0 k)"
"sub (Bit0 k) (Bit0 l) = dbl (sub k l)"
"sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
"sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
"sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
- by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
+ by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def numeral.simps
numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
lemma add_neg_numeral_simps:
- "numeral m + neg_numeral n = sub m n"
- "neg_numeral m + numeral n = sub n m"
- "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
- by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
+ "numeral m + - numeral n = sub m n"
+ "- numeral m + numeral n = sub n m"
+ "- numeral m + - numeral n = - (numeral m + numeral n)"
+ by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
del: add_uminus_conv_diff add: diff_conv_add_uminus)
lemma add_neg_numeral_special:
- "1 + neg_numeral m = sub One m"
- "neg_numeral m + 1 = sub One m"
- by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
+ "1 + - numeral m = sub One m"
+ "- numeral m + 1 = sub One m"
+ "numeral m + - 1 = sub m One"
+ "- 1 + numeral n = sub n One"
+ "- 1 + - numeral n = - numeral (inc n)"
+ "- numeral m + - 1 = - numeral (inc m)"
+ "1 + - 1 = 0"
+ "- 1 + 1 = 0"
+ "- 1 + - 1 = - 2"
+ by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc
+ del: add_uminus_conv_diff add: diff_conv_add_uminus)
lemma diff_numeral_simps:
"numeral m - numeral n = sub m n"
- "numeral m - neg_numeral n = numeral (m + n)"
- "neg_numeral m - numeral n = neg_numeral (m + n)"
- "neg_numeral m - neg_numeral n = sub n m"
- by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
+ "numeral m - - numeral n = numeral (m + n)"
+ "- numeral m - numeral n = - numeral (m + n)"
+ "- numeral m - - numeral n = sub n m"
+ by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize
del: add_uminus_conv_diff add: diff_conv_add_uminus)
lemma diff_numeral_special:
"1 - numeral n = sub One n"
- "1 - neg_numeral n = numeral (One + n)"
"numeral m - 1 = sub m One"
- "neg_numeral m - 1 = neg_numeral (m + One)"
- by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
-
-lemma minus_one: "- 1 = -1"
- unfolding neg_numeral_def numeral.simps ..
-
-lemma minus_numeral: "- numeral n = neg_numeral n"
- unfolding neg_numeral_def ..
-
-lemma minus_neg_numeral: "- neg_numeral n = numeral n"
- unfolding neg_numeral_def by simp
-
-lemmas minus_numeral_simps [simp] =
- minus_one minus_numeral minus_neg_numeral
+ "1 - - numeral n = numeral (One + n)"
+ "- numeral m - 1 = - numeral (m + One)"
+ "- 1 - numeral n = - numeral (inc n)"
+ "numeral m - - 1 = numeral (inc m)"
+ "- 1 - - numeral n = sub n One"
+ "- numeral m - - 1 = sub One m"
+ "1 - 1 = 0"
+ "- 1 - 1 = - 2"
+ "1 - - 1 = 2"
+ "- 1 - - 1 = 0"
+ by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc
+ del: add_uminus_conv_diff add: diff_conv_add_uminus)
end
@@ -675,17 +677,17 @@
subclass neg_numeral ..
lemma mult_neg_numeral_simps:
- "neg_numeral m * neg_numeral n = numeral (m * n)"
- "neg_numeral m * numeral n = neg_numeral (m * n)"
- "numeral m * neg_numeral n = neg_numeral (m * n)"
- unfolding neg_numeral_def mult_minus_left mult_minus_right
+ "- numeral m * - numeral n = numeral (m * n)"
+ "- numeral m * numeral n = - numeral (m * n)"
+ "numeral m * - numeral n = - numeral (m * n)"
+ unfolding mult_minus_left mult_minus_right
by (simp_all only: minus_minus numeral_mult)
-lemma mult_minus1 [simp]: "-1 * z = - z"
- unfolding neg_numeral_def numeral.simps mult_minus_left by simp
+lemma mult_minus1 [simp]: "- 1 * z = - z"
+ unfolding numeral.simps mult_minus_left by simp
-lemma mult_minus1_right [simp]: "z * -1 = - z"
- unfolding neg_numeral_def numeral.simps mult_minus_right by simp
+lemma mult_minus1_right [simp]: "z * - 1 = - z"
+ unfolding numeral.simps mult_minus_right by simp
end
@@ -708,9 +710,15 @@
lemma not_iszero_Numeral1: "\<not> iszero Numeral1"
by (simp add: numeral_One)
+lemma not_iszero_neg_1 [simp]: "\<not> iszero (- 1)"
+ by (simp add: iszero_def)
+
+lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)"
+ by (simp add: numeral_One)
+
lemma iszero_neg_numeral [simp]:
- "iszero (neg_numeral w) \<longleftrightarrow> iszero (numeral w)"
- unfolding iszero_def neg_numeral_def
+ "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)"
+ unfolding iszero_def
by (rule neg_equal_0_iff_equal)
lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)"
@@ -730,17 +738,17 @@
lemma eq_numeral_iff_iszero:
"numeral x = numeral y \<longleftrightarrow> iszero (sub x y)"
- "numeral x = neg_numeral y \<longleftrightarrow> iszero (numeral (x + y))"
- "neg_numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
- "neg_numeral x = neg_numeral y \<longleftrightarrow> iszero (sub y x)"
+ "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))"
+ "- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))"
+ "- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)"
"numeral x = 1 \<longleftrightarrow> iszero (sub x One)"
"1 = numeral y \<longleftrightarrow> iszero (sub One y)"
- "neg_numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
- "1 = neg_numeral y \<longleftrightarrow> iszero (numeral (One + y))"
+ "- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))"
+ "1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))"
"numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
"0 = numeral y \<longleftrightarrow> iszero (numeral y)"
- "neg_numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
- "0 = neg_numeral y \<longleftrightarrow> iszero (numeral y)"
+ "- numeral x = 0 \<longleftrightarrow> iszero (numeral x)"
+ "0 = - numeral y \<longleftrightarrow> iszero (numeral y)"
unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special
by simp_all
@@ -756,33 +764,69 @@
lemma not_iszero_numeral [simp]: "\<not> iszero (numeral w)"
by (simp add: iszero_def)
-lemma neg_numeral_eq_iff: "neg_numeral m = neg_numeral n \<longleftrightarrow> m = n"
- by (simp only: neg_numeral_def neg_equal_iff_equal numeral_eq_iff)
+lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n"
+ by simp
-lemma numeral_neq_neg_numeral: "numeral m \<noteq> neg_numeral n"
- unfolding neg_numeral_def eq_neg_iff_add_eq_0
+lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n"
+ unfolding eq_neg_iff_add_eq_0
by (simp add: numeral_plus_numeral)
-lemma neg_numeral_neq_numeral: "neg_numeral m \<noteq> numeral n"
+lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n"
by (rule numeral_neq_neg_numeral [symmetric])
-lemma zero_neq_neg_numeral: "0 \<noteq> neg_numeral n"
- unfolding neg_numeral_def neg_0_equal_iff_equal by simp
+lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n"
+ unfolding neg_0_equal_iff_equal by simp
-lemma neg_numeral_neq_zero: "neg_numeral n \<noteq> 0"
- unfolding neg_numeral_def neg_equal_0_iff_equal by simp
+lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0"
+ unfolding neg_equal_0_iff_equal by simp
-lemma one_neq_neg_numeral: "1 \<noteq> neg_numeral n"
+lemma one_neq_neg_numeral: "1 \<noteq> - numeral n"
using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One)
-lemma neg_numeral_neq_one: "neg_numeral n \<noteq> 1"
+lemma neg_numeral_neq_one: "- numeral n \<noteq> 1"
using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One)
+lemma neg_one_neq_numeral:
+ "- 1 \<noteq> numeral n"
+ using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One)
+
+lemma numeral_neq_neg_one:
+ "numeral n \<noteq> - 1"
+ using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One)
+
+lemma neg_one_eq_numeral_iff:
+ "- 1 = - numeral n \<longleftrightarrow> n = One"
+ using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One)
+
+lemma numeral_eq_neg_one_iff:
+ "- numeral n = - 1 \<longleftrightarrow> n = One"
+ using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One)
+
+lemma neg_one_neq_zero:
+ "- 1 \<noteq> 0"
+ by simp
+
+lemma zero_neq_neg_one:
+ "0 \<noteq> - 1"
+ by simp
+
+lemma neg_one_neq_one:
+ "- 1 \<noteq> 1"
+ using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
+
+lemma one_neq_neg_one:
+ "1 \<noteq> - 1"
+ using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True)
+
lemmas eq_neg_numeral_simps [simp] =
neg_numeral_eq_iff
numeral_neq_neg_numeral neg_numeral_neq_numeral
one_neq_neg_numeral neg_numeral_neq_one
zero_neq_neg_numeral neg_numeral_neq_zero
+ neg_one_neq_numeral numeral_neq_neg_one
+ neg_one_eq_numeral_iff numeral_eq_neg_one_iff
+ neg_one_neq_zero zero_neq_neg_one
+ neg_one_neq_one one_neq_neg_one
end
@@ -795,48 +839,72 @@
subclass ring_char_0 ..
-lemma neg_numeral_le_iff: "neg_numeral m \<le> neg_numeral n \<longleftrightarrow> n \<le> m"
- by (simp only: neg_numeral_def neg_le_iff_le numeral_le_iff)
+lemma neg_numeral_le_iff: "- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m"
+ by (simp only: neg_le_iff_le numeral_le_iff)
-lemma neg_numeral_less_iff: "neg_numeral m < neg_numeral n \<longleftrightarrow> n < m"
- by (simp only: neg_numeral_def neg_less_iff_less numeral_less_iff)
+lemma neg_numeral_less_iff: "- numeral m < - numeral n \<longleftrightarrow> n < m"
+ by (simp only: neg_less_iff_less numeral_less_iff)
-lemma neg_numeral_less_zero: "neg_numeral n < 0"
- by (simp only: neg_numeral_def neg_less_0_iff_less zero_less_numeral)
+lemma neg_numeral_less_zero: "- numeral n < 0"
+ by (simp only: neg_less_0_iff_less zero_less_numeral)
-lemma neg_numeral_le_zero: "neg_numeral n \<le> 0"
- by (simp only: neg_numeral_def neg_le_0_iff_le zero_le_numeral)
+lemma neg_numeral_le_zero: "- numeral n \<le> 0"
+ by (simp only: neg_le_0_iff_le zero_le_numeral)
-lemma not_zero_less_neg_numeral: "\<not> 0 < neg_numeral n"
+lemma not_zero_less_neg_numeral: "\<not> 0 < - numeral n"
by (simp only: not_less neg_numeral_le_zero)
-lemma not_zero_le_neg_numeral: "\<not> 0 \<le> neg_numeral n"
+lemma not_zero_le_neg_numeral: "\<not> 0 \<le> - numeral n"
by (simp only: not_le neg_numeral_less_zero)
-lemma neg_numeral_less_numeral: "neg_numeral m < numeral n"
+lemma neg_numeral_less_numeral: "- numeral m < numeral n"
using neg_numeral_less_zero zero_less_numeral by (rule less_trans)
-lemma neg_numeral_le_numeral: "neg_numeral m \<le> numeral n"
+lemma neg_numeral_le_numeral: "- numeral m \<le> numeral n"
by (simp only: less_imp_le neg_numeral_less_numeral)
-lemma not_numeral_less_neg_numeral: "\<not> numeral m < neg_numeral n"
+lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n"
by (simp only: not_less neg_numeral_le_numeral)
-lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> neg_numeral n"
+lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n"
by (simp only: not_le neg_numeral_less_numeral)
-lemma neg_numeral_less_one: "neg_numeral m < 1"
+lemma neg_numeral_less_one: "- numeral m < 1"
by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One])
-lemma neg_numeral_le_one: "neg_numeral m \<le> 1"
+lemma neg_numeral_le_one: "- numeral m \<le> 1"
by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One])
-lemma not_one_less_neg_numeral: "\<not> 1 < neg_numeral m"
+lemma not_one_less_neg_numeral: "\<not> 1 < - numeral m"
by (simp only: not_less neg_numeral_le_one)
-lemma not_one_le_neg_numeral: "\<not> 1 \<le> neg_numeral m"
+lemma not_one_le_neg_numeral: "\<not> 1 \<le> - numeral m"
by (simp only: not_le neg_numeral_less_one)
+lemma not_numeral_less_neg_one: "\<not> numeral m < - 1"
+ using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One)
+
+lemma not_numeral_le_neg_one: "\<not> numeral m \<le> - 1"
+ using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One)
+
+lemma neg_one_less_numeral: "- 1 < numeral m"
+ using neg_numeral_less_numeral [of One m] by (simp add: numeral_One)
+
+lemma neg_one_le_numeral: "- 1 \<le> numeral m"
+ using neg_numeral_le_numeral [of One m] by (simp add: numeral_One)
+
+lemma neg_numeral_less_neg_one_iff: "- numeral m < - 1 \<longleftrightarrow> m \<noteq> One"
+ by (cases m) simp_all
+
+lemma neg_numeral_le_neg_one: "- numeral m \<le> - 1"
+ by simp
+
+lemma not_neg_one_less_neg_numeral: "\<not> - 1 < - numeral m"
+ by simp
+
+lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One"
+ by (cases m) simp_all
+
lemma sub_non_negative:
"sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m"
by (simp only: sub_def le_diff_eq) simp
@@ -858,18 +926,40 @@
neg_numeral_le_numeral not_numeral_le_neg_numeral
neg_numeral_le_zero not_zero_le_neg_numeral
neg_numeral_le_one not_one_le_neg_numeral
+ neg_one_le_numeral not_numeral_le_neg_one
+ neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff
+
+lemma le_minus_one_simps [simp]:
+ "- 1 \<le> 0"
+ "- 1 \<le> 1"
+ "\<not> 0 \<le> - 1"
+ "\<not> 1 \<le> - 1"
+ by simp_all
lemmas less_neg_numeral_simps [simp] =
neg_numeral_less_iff
neg_numeral_less_numeral not_numeral_less_neg_numeral
neg_numeral_less_zero not_zero_less_neg_numeral
neg_numeral_less_one not_one_less_neg_numeral
+ neg_one_less_numeral not_numeral_less_neg_one
+ neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral
+
+lemma less_minus_one_simps [simp]:
+ "- 1 < 0"
+ "- 1 < 1"
+ "\<not> 0 < - 1"
+ "\<not> 1 < - 1"
+ by (simp_all add: less_le)
lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
by simp
-lemma abs_neg_numeral [simp]: "abs (neg_numeral n) = numeral n"
- by (simp only: neg_numeral_def abs_minus_cancel abs_numeral)
+lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n"
+ by (simp only: abs_minus_cancel abs_numeral)
+
+lemma abs_neg_one [simp]:
+ "abs (- 1) = 1"
+ by simp
end
@@ -1032,31 +1122,36 @@
text{*Theorem lists for the cancellation simprocs. The use of a binary
numeral for 1 reduces the number of special cases.*}
-lemmas mult_1s =
- mult_numeral_1 mult_numeral_1_right
- mult_minus1 mult_minus1_right
+lemma mult_1s:
+ fixes a :: "'a::semiring_numeral"
+ and b :: "'b::ring_1"
+ shows "Numeral1 * a = a"
+ "a * Numeral1 = a"
+ "- Numeral1 * b = - b"
+ "b * - Numeral1 = - b"
+ by simp_all
setup {*
Reorient_Proc.add
(fn Const (@{const_name numeral}, _) $ _ => true
- | Const (@{const_name neg_numeral}, _) $ _ => true
+ | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true
| _ => false)
*}
simproc_setup reorient_numeral
- ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
+ ("numeral w = x" | "- numeral w = y") = Reorient_Proc.proc
subsubsection {* Simplification of arithmetic operations on integer constants. *}
lemmas arith_special = (* already declared simp above *)
add_numeral_special add_neg_numeral_special
- diff_numeral_special minus_one
+ diff_numeral_special
(* rules already in simpset *)
lemmas arith_extra_simps =
numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right
- minus_numeral minus_neg_numeral minus_zero minus_one
+ minus_zero
diff_numeral_simps diff_0 diff_0_right
numeral_times_numeral mult_neg_numeral_simps
mult_zero_left mult_zero_right
@@ -1089,15 +1184,15 @@
lemmas rel_simps =
le_num_simps less_num_simps eq_num_simps
- le_numeral_simps le_neg_numeral_simps le_numeral_extra
- less_numeral_simps less_neg_numeral_simps less_numeral_extra
+ le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra
+ less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra
eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
-lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
+lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
-- {* Unfold all @{text let}s involving constants *}
unfolding Let_def ..
@@ -1133,16 +1228,16 @@
by (simp_all add: add_assoc [symmetric])
lemma add_neg_numeral_left [simp]:
- "numeral v + (neg_numeral w + y) = (sub v w + y)"
- "neg_numeral v + (numeral w + y) = (sub w v + y)"
- "neg_numeral v + (neg_numeral w + y) = (neg_numeral(v + w) + y)"
+ "numeral v + (- numeral w + y) = (sub v w + y)"
+ "- numeral v + (numeral w + y) = (sub w v + y)"
+ "- numeral v + (- numeral w + y) = (- numeral(v + w) + y)"
by (simp_all add: add_assoc [symmetric])
lemma mult_numeral_left [simp]:
"numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)"
- "neg_numeral v * (numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
- "numeral v * (neg_numeral w * y) = (neg_numeral(v * w) * y :: 'b::ring_1)"
- "neg_numeral v * (neg_numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
+ "- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
+ "numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'b::ring_1)"
+ "- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'b::ring_1)"
by (simp_all add: mult_assoc [symmetric])
hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec
--- a/src/HOL/Number_Theory/Cong.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Tue Nov 19 10:05:53 2013 +0100
@@ -323,8 +323,6 @@
\<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
apply (simp only: cong_altdef_int)
apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
- (* any way around this? *)
- apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
apply (auto simp add: field_simps)
done
@@ -665,7 +663,6 @@
apply auto
apply (cases "n \<ge> 0")
apply auto
- apply (subst cong_int_def, auto)
apply (frule cong_solve_int [of a n])
apply auto
done
--- a/src/HOL/Number_Theory/Residues.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Tue Nov 19 10:05:53 2013 +0100
@@ -455,6 +455,7 @@
apply (subst fact_altdef_int, simp)
apply (subst cong_int_def)
apply simp
+ apply arith
apply (rule residues_prime.wilson_theorem1)
apply (rule residues_prime.intro)
apply auto
--- a/src/HOL/Numeral_Simprocs.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Tue Nov 19 10:05:53 2013 +0100
@@ -17,7 +17,7 @@
if_False if_True
add_0 add_Suc add_numeral_left
add_neg_numeral_left mult_numeral_left
- numeral_1_eq_1 [symmetric] Suc_eq_plus1
+ numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
eq_numeral_iff_iszero not_iszero_Numeral1
declare split_div [of _ _ "numeral k", arith_split] for k
@@ -85,18 +85,19 @@
text {* For @{text cancel_factor} *}
-lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)"
-by auto
+lemmas nat_mult_le_cancel_disj = mult_le_cancel1
-lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)"
-by auto
+lemmas nat_mult_less_cancel_disj = mult_less_cancel1
-lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
-by auto
+lemma nat_mult_eq_cancel_disj:
+ fixes k m n :: nat
+ shows "k * m = k * n \<longleftrightarrow> k = 0 \<or> m = n"
+ by auto
-lemma nat_mult_div_cancel_disj[simp]:
- "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
-by (simp add: nat_mult_div_cancel1)
+lemma nat_mult_div_cancel_disj [simp]:
+ fixes k m n :: nat
+ shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
+ by (fact div_mult_mult1_if)
ML_file "Tools/numeral_simprocs.ML"
--- a/src/HOL/Parity.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Parity.thy Tue Nov 19 10:05:53 2013 +0100
@@ -78,7 +78,7 @@
unfolding even_def by simp
(* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
-declare even_def [of "neg_numeral v", simp] for v
+declare even_def [of "- numeral v", simp] for v
lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
unfolding even_nat_def by simp
@@ -190,14 +190,9 @@
by (induct n) simp_all
lemma (in comm_ring_1)
- shows minus_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
- and minus_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
- by (simp_all add: neg_power_if del: minus_one)
-
-lemma (in comm_ring_1)
- shows neg_one_even_power [simp]: "even n \<Longrightarrow> (-1) ^ n = 1"
- and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (-1) ^ n = - 1"
- by (simp_all add: minus_one [symmetric] del: minus_one)
+ shows neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
+ and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
+ by (simp_all add: neg_power_if)
lemma zero_le_even_power: "even n ==>
0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
--- a/src/HOL/Power.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Power.thy Tue Nov 19 10:05:53 2013 +0100
@@ -209,14 +209,6 @@
"(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
-lemma power_neg_numeral_Bit0 [simp]:
- "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"
- by (simp only: neg_numeral_def power_minus_Bit0 power_numeral)
-
-lemma power_neg_numeral_Bit1 [simp]:
- "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))"
- by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
-
lemma power2_minus [simp]:
"(- a)\<^sup>2 = a\<^sup>2"
by (rule power_minus_Bit0)
--- a/src/HOL/Rat.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Rat.thy Tue Nov 19 10:05:53 2013 +0100
@@ -215,17 +215,19 @@
"Fract 0 k = 0"
"Fract 1 1 = 1"
"Fract (numeral w) 1 = numeral w"
- "Fract (neg_numeral w) 1 = neg_numeral w"
+ "Fract (- numeral w) 1 = - numeral w"
+ "Fract (- 1) 1 = - 1"
"Fract k 0 = 0"
using Fract_of_int_eq [of "numeral w"]
- using Fract_of_int_eq [of "neg_numeral w"]
+ using Fract_of_int_eq [of "- numeral w"]
by (simp_all add: Zero_rat_def One_rat_def eq_rat)
lemma rat_number_expand:
"0 = Fract 0 1"
"1 = Fract 1 1"
"numeral k = Fract (numeral k) 1"
- "neg_numeral k = Fract (neg_numeral k) 1"
+ "- 1 = Fract (- 1) 1"
+ "- numeral k = Fract (- numeral k) 1"
by (simp_all add: rat_number_collapse)
lemma Rat_cases_nonzero [case_names Fract 0]:
@@ -356,7 +358,8 @@
"quotient_of 0 = (0, 1)"
"quotient_of 1 = (1, 1)"
"quotient_of (numeral k) = (numeral k, 1)"
- "quotient_of (neg_numeral k) = (neg_numeral k, 1)"
+ "quotient_of (- 1) = (- 1, 1)"
+ "quotient_of (- numeral k) = (- numeral k, 1)"
by (simp_all add: rat_number_expand quotient_of_Fract)
lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
@@ -620,7 +623,7 @@
#> Lin_Arith.add_simps [@{thm neg_less_iff_less},
@{thm True_implies_equals},
read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
- read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left},
+ read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
@@ -664,6 +667,10 @@
lemma of_rat_minus: "of_rat (- a) = - of_rat a"
by transfer simp
+lemma of_rat_neg_one [simp]:
+ "of_rat (- 1) = - 1"
+ by (simp add: of_rat_minus)
+
lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
using of_rat_add [of a "- b"] by (simp add: of_rat_minus)
@@ -778,8 +785,8 @@
using of_rat_of_int_eq [of "numeral w"] by simp
lemma of_rat_neg_numeral_eq [simp]:
- "of_rat (neg_numeral w) = neg_numeral w"
-using of_rat_of_int_eq [of "neg_numeral w"] by simp
+ "of_rat (- numeral w) = - numeral w"
+using of_rat_of_int_eq [of "- numeral w"] by simp
lemmas zero_rat = Zero_rat_def
lemmas one_rat = One_rat_def
@@ -820,9 +827,6 @@
lemma Rats_number_of [simp]: "numeral w \<in> Rats"
by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
-lemma Rats_neg_number_of [simp]: "neg_numeral w \<in> Rats"
-by (subst of_rat_neg_numeral_eq [symmetric], rule Rats_of_rat)
-
lemma Rats_0 [simp]: "0 \<in> Rats"
apply (unfold Rats_def)
apply (rule range_eqI)
@@ -943,7 +947,7 @@
by (simp add: Rat.of_int_def)
lemma [code_unfold]:
- "neg_numeral k = Rat.of_int (neg_numeral k)"
+ "- numeral k = Rat.of_int (- numeral k)"
by (simp add: Rat.of_int_def)
lemma Frct_code_post [code_post]:
@@ -951,13 +955,13 @@
"Frct (a, 0) = 0"
"Frct (1, 1) = 1"
"Frct (numeral k, 1) = numeral k"
- "Frct (neg_numeral k, 1) = neg_numeral k"
+ "Frct (- numeral k, 1) = - numeral k"
"Frct (1, numeral k) = 1 / numeral k"
- "Frct (1, neg_numeral k) = 1 / neg_numeral k"
+ "Frct (1, - numeral k) = 1 / - numeral k"
"Frct (numeral k, numeral l) = numeral k / numeral l"
- "Frct (numeral k, neg_numeral l) = numeral k / neg_numeral l"
- "Frct (neg_numeral k, numeral l) = neg_numeral k / numeral l"
- "Frct (neg_numeral k, neg_numeral l) = neg_numeral k / neg_numeral l"
+ "Frct (numeral k, - numeral l) = numeral k / - numeral l"
+ "Frct (- numeral k, numeral l) = - numeral k / numeral l"
+ "Frct (- numeral k, - numeral l) = - numeral k / - numeral l"
by (simp_all add: Fract_of_int_quotient)
@@ -1156,7 +1160,7 @@
in
if i = 0 then Syntax.const @{const_syntax Groups.zero}
else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
- else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
+ else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
end;
fun mk_frac str =
--- a/src/HOL/Real.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Real.thy Tue Nov 19 10:05:53 2013 +0100
@@ -1447,13 +1447,13 @@
lemma [code_abbrev]:
"real_of_int (numeral k) = numeral k"
- "real_of_int (neg_numeral k) = neg_numeral k"
+ "real_of_int (- numeral k) = - numeral k"
by simp_all
-text{*Collapse applications of @{term real} to @{term number_of}*}
+text{*Collapse applications of @{const real} to @{const numeral}*}
lemma real_numeral [simp]:
"real (numeral v :: int) = numeral v"
- "real (neg_numeral v :: int) = neg_numeral v"
+ "real (- numeral v :: int) = - numeral v"
by (simp_all add: real_of_int_def)
lemma real_of_nat_numeral [simp]:
@@ -1559,11 +1559,11 @@
unfolding real_of_int_le_iff[symmetric] by simp
lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:
- "(neg_numeral x::real) ^ n \<le> real a \<longleftrightarrow> (neg_numeral x::int) ^ n \<le> a"
+ "(- numeral x::real) ^ n \<le> real a \<longleftrightarrow> (- numeral x::int) ^ n \<le> a"
unfolding real_of_int_le_iff[symmetric] by simp
lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:
- "real a \<le> (neg_numeral x::real) ^ n \<longleftrightarrow> a \<le> (neg_numeral x::int) ^ n"
+ "real a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
unfolding real_of_int_le_iff[symmetric] by simp
subsection{*Density of the Reals*}
@@ -2051,7 +2051,7 @@
by simp
lemma [code_abbrev]:
- "(of_rat (neg_numeral k) :: real) = neg_numeral k"
+ "(of_rat (- numeral k) :: real) = - numeral k"
by simp
lemma [code_post]:
@@ -2059,14 +2059,14 @@
"(of_rat (r / 0) :: real) = 0"
"(of_rat (1 / 1) :: real) = 1"
"(of_rat (numeral k / 1) :: real) = numeral k"
- "(of_rat (neg_numeral k / 1) :: real) = neg_numeral k"
+ "(of_rat (- numeral k / 1) :: real) = - numeral k"
"(of_rat (1 / numeral k) :: real) = 1 / numeral k"
- "(of_rat (1 / neg_numeral k) :: real) = 1 / neg_numeral k"
+ "(of_rat (1 / - numeral k) :: real) = 1 / - numeral k"
"(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l"
- "(of_rat (numeral k / neg_numeral l) :: real) = numeral k / neg_numeral l"
- "(of_rat (neg_numeral k / numeral l) :: real) = neg_numeral k / numeral l"
- "(of_rat (neg_numeral k / neg_numeral l) :: real) = neg_numeral k / neg_numeral l"
- by (simp_all add: of_rat_divide)
+ "(of_rat (numeral k / - numeral l) :: real) = numeral k / - numeral l"
+ "(of_rat (- numeral k / numeral l) :: real) = - numeral k / numeral l"
+ "(of_rat (- numeral k / - numeral l) :: real) = - numeral k / - numeral l"
+ by (simp_all add: of_rat_divide of_rat_minus)
text {* Operations *}
--- a/src/HOL/Real_Vector_Spaces.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Nov 19 10:05:53 2013 +0100
@@ -307,8 +307,8 @@
lemma of_real_numeral: "of_real (numeral w) = numeral w"
using of_real_of_int_eq [of "numeral w"] by simp
-lemma of_real_neg_numeral: "of_real (neg_numeral w) = neg_numeral w"
-using of_real_of_int_eq [of "neg_numeral w"] by simp
+lemma of_real_neg_numeral: "of_real (- numeral w) = - numeral w"
+using of_real_of_int_eq [of "- numeral w"] by simp
text{*Every real algebra has characteristic zero*}
@@ -341,9 +341,6 @@
lemma Reals_numeral [simp]: "numeral w \<in> Reals"
by (subst of_real_numeral [symmetric], rule Reals_of_real)
-lemma Reals_neg_numeral [simp]: "neg_numeral w \<in> Reals"
-by (subst of_real_neg_numeral [symmetric], rule Reals_of_real)
-
lemma Reals_0 [simp]: "0 \<in> Reals"
apply (unfold Reals_def)
apply (rule range_eqI)
@@ -602,7 +599,7 @@
by (subst of_real_numeral [symmetric], subst norm_of_real, simp)
lemma norm_neg_numeral [simp]:
- "norm (neg_numeral w::'a::real_normed_algebra_1) = numeral w"
+ "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
lemma norm_of_int [simp]:
--- a/src/HOL/Rings.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Rings.thy Tue Nov 19 10:05:53 2013 +0100
@@ -1058,6 +1058,34 @@
"\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
by(subst abs_dvd_iff[symmetric]) simp
+text {* The following lemmas can be proven in more generale structures, but
+are dangerous as simp rules in absence of @{thm neg_equal_zero},
+@{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
+
+lemma equation_minus_iff_1 [simp, no_atp]:
+ "1 = - a \<longleftrightarrow> a = - 1"
+ by (fact equation_minus_iff)
+
+lemma minus_equation_iff_1 [simp, no_atp]:
+ "- a = 1 \<longleftrightarrow> a = - 1"
+ by (subst minus_equation_iff, auto)
+
+lemma le_minus_iff_1 [simp, no_atp]:
+ "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
+ by (fact le_minus_iff)
+
+lemma minus_le_iff_1 [simp, no_atp]:
+ "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
+ by (fact minus_le_iff)
+
+lemma less_minus_iff_1 [simp, no_atp]:
+ "1 < - b \<longleftrightarrow> b < - 1"
+ by (fact less_minus_iff)
+
+lemma minus_less_iff_1 [simp, no_atp]:
+ "- a < 1 \<longleftrightarrow> - 1 < a"
+ by (fact minus_less_iff)
+
end
text {* Simprules for comparisons where common factors can be cancelled. *}
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Nov 19 10:05:53 2013 +0100
@@ -374,7 +374,6 @@
lemma
"(0::int) = 0"
- "(0::int) = -0"
"(0::int) = (- 0)"
"(1::int) = 1"
"\<not>(-1 = (1::int))"
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs Tue Nov 19 10:05:53 2013 +0100
@@ -54,3 +54,5 @@
unsat
e5c27ae0a583eeafeaa4ef3c59b1b4ec53e06b0f 1 0
unsat
+7d3ef49480d3ed3a7e5f2d7a12e7108cf7fc7819 1 0
+unsat
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Nov 19 10:05:53 2013 +0100
@@ -1645,10 +1645,10 @@
(hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
def_tables, ground_thm_table, ersatz_table, ...}) =
let
- fun do_numeral depth Ts mult T t0 t1 =
+ fun do_numeral depth Ts mult T some_t0 t1 t2 =
(if is_number_type ctxt T then
let
- val j = mult * HOLogic.dest_num t1
+ val j = mult * HOLogic.dest_num t2
in
if j = 1 then
raise SAME ()
@@ -1667,15 +1667,16 @@
handle TERM _ => raise SAME ()
else
raise SAME ())
- handle SAME () => s_betapply [] (do_term depth Ts t0, do_term depth Ts t1)
+ handle SAME () => (case some_t0 of NONE => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)
+ | SOME t0 => s_betapply [] (do_term depth Ts t0, s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)))
and do_term depth Ts t =
case t of
- (t0 as Const (@{const_name Num.neg_numeral_class.neg_numeral},
- Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
- do_numeral depth Ts ~1 ran_T t0 t1
- | (t0 as Const (@{const_name Num.numeral_class.numeral},
- Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
- do_numeral depth Ts 1 ran_T t0 t1
+ (t0 as Const (@{const_name uminus}, _) $ ((t1 as Const (@{const_name numeral},
+ Type (@{type_name fun}, [_, ran_T]))) $ t2)) =>
+ do_numeral depth Ts ~1 ran_T (SOME t0) t1 t2
+ | (t1 as Const (@{const_name numeral},
+ Type (@{type_name fun}, [_, ran_T]))) $ t2 =>
+ do_numeral depth Ts 1 ran_T NONE t1 t2
| Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
| (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Nov 19 10:05:53 2013 +0100
@@ -42,7 +42,6 @@
@{term "nat"}, @{term "int"},
@{term "Num.One"}, @{term "Num.Bit0"}, @{term "Num.Bit1"},
@{term "Num.numeral :: num => int"}, @{term "Num.numeral :: num => nat"},
- @{term "Num.neg_numeral :: num => int"},
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
@{term "True"}, @{term "False"}];
@@ -610,8 +609,6 @@
| num_of_term vs @{term "1::int"} = Proc.C (Proc.Int_of_integer 1)
| num_of_term vs (t as Const (@{const_name numeral}, _) $ _) =
Proc.C (Proc.Int_of_integer (dest_number t))
- | num_of_term vs (t as Const (@{const_name neg_numeral}, _) $ _) =
- Proc.Neg (Proc.C (Proc.Int_of_integer (dest_number t)))
| num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
Proc.Neg (num_of_term vs t')
| num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
--- a/src/HOL/Tools/SMT/smt_builtin.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Nov 19 10:05:53 2013 +0100
@@ -144,9 +144,10 @@
(case try HOLogic.dest_number t of
NONE => NONE
| SOME (T, i) =>
- (case lookup_builtin_typ ctxt T of
- SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
- | _ => NONE))
+ if i < 0 then NONE else
+ (case lookup_builtin_typ ctxt T of
+ SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
+ | _ => NONE))
val is_builtin_num = is_some oo dest_builtin_num
--- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Nov 19 10:05:53 2013 +0100
@@ -526,23 +526,26 @@
local
(*
- rewrite negative numerals into positive numerals,
- rewrite Numeral0 into 0
rewrite Numeral1 into 1
+ rewrite - 0 into 0
*)
- fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) =
- SMT_Builtin.is_builtin_num ctxt t
- | is_strange_number _ _ = false
+ fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) =
+ true
+ | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
+ true
+ | is_irregular_number _ =
+ false;
- val pos_num_ss =
+ fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t;
+
+ val proper_num_ss =
simpset_of (put_simpset HOL_ss @{context}
- addsimps [@{thm Num.numeral_One}]
- addsimps [@{thm Num.neg_numeral_def}])
+ addsimps @{thms Num.numeral_One minus_zero})
fun norm_num_conv ctxt =
SMT_Utils.if_conv (is_strange_number ctxt)
- (Simplifier.rewrite (put_simpset pos_num_ss ctxt)) Conv.no_conv
+ (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
in
fun normalize_numerals_conv ctxt =
--- a/src/HOL/Tools/SMT/smt_utils.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML Tue Nov 19 10:05:53 2013 +0100
@@ -140,7 +140,6 @@
is_num env t andalso is_num env u
| is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) =
is_num (t :: env) u
- | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t
| is_num env (Bound i) = i < length env andalso is_num env (nth env i)
| is_num _ t = can HOLogic.dest_number t
in is_num [] end
--- a/src/HOL/Tools/hologic.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/hologic.ML Tue Nov 19 10:05:53 2013 +0100
@@ -104,7 +104,6 @@
val mk_numeral: int -> term
val dest_num: term -> int
val numeral_const: typ -> term
- val neg_numeral_const: typ -> term
val add_numerals: term -> (term * typ) list -> (term * typ) list
val mk_number: typ -> int -> term
val dest_number: term -> typ * int
@@ -548,7 +547,6 @@
| dest_num t = raise TERM ("dest_num", [t]);
fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T);
-fun neg_numeral_const T = Const ("Num.neg_numeral_class.neg_numeral", numT --> T);
fun add_numerals (Const ("Num.numeral_class.numeral", Type (_, [_, T])) $ t) = cons (t, T)
| add_numerals (t $ u) = add_numerals t #> add_numerals u
@@ -559,14 +557,14 @@
| mk_number T 1 = Const ("Groups.one_class.one", T)
| mk_number T i =
if i > 0 then numeral_const T $ mk_numeral i
- else neg_numeral_const T $ mk_numeral (~ i);
+ else Const ("Groups.uminus_class.uminus", T --> T) $ mk_number T (~ i);
fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
| dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
| dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
(T, dest_num t)
- | dest_number (Const ("Num.neg_numeral_class.neg_numeral", Type ("fun", [_, T])) $ t) =
- (T, ~ (dest_num t))
+ | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
+ apsnd (op ~) (dest_number t)
| dest_number t = raise TERM ("dest_number", [t]);
--- a/src/HOL/Tools/lin_arith.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/lin_arith.ML Tue Nov 19 10:05:53 2013 +0100
@@ -183,9 +183,6 @@
| demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) =
((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_num n)))
handle TERM _ => (SOME t, m))
- | demult (t as Const ("Num.neg_numeral_class.neg_numeral", _) $ n, m) =
- ((NONE, Rat.mult m (Rat.rat_of_int (~ (HOLogic.dest_num n))))
- handle TERM _ => (SOME t, m))
| demult (t as Const (@{const_name Suc}, _) $ _, m) =
((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
handle TERM _ => (SOME t, m))
@@ -212,6 +209,10 @@
pi
| poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
(p, Rat.add i m)
+ | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
+ (let val k = HOLogic.dest_num t
+ in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
+ handle TERM _ => add_atom all m pi)
| poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
poly (t, m, (p, Rat.add i m))
| poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) =
@@ -222,14 +223,6 @@
(case demult inj_consts (all, m) of
(NONE, m') => (p, Rat.add i m')
| (SOME u, m') => add_atom u m' pi)
- | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
- (let val k = HOLogic.dest_num t
- in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
- handle TERM _ => add_atom all m pi)
- | poly (all as Const ("Num.neg_numeral_class.neg_numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
- (let val k = HOLogic.dest_num t
- in (p, Rat.add i (Rat.mult m (Rat.rat_of_int (~ k)))) end
- handle TERM _ => add_atom all m pi)
| poly (all as Const f $ x, m, pi) =
if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
| poly (all, m, pi) =
--- a/src/HOL/Tools/numeral.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/numeral.ML Tue Nov 19 10:05:53 2013 +0100
@@ -45,8 +45,8 @@
val numeral = @{cpat "numeral"};
val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
-val neg_numeral = @{cpat "neg_numeral"};
-val neg_numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term neg_numeral)));
+val uminus = @{cpat "uminus"};
+val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus)));
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
@@ -56,7 +56,7 @@
| mk_cnumber T 1 = instT T oneT one
| mk_cnumber T i =
if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
- else Thm.apply (instT T neg_numeralT neg_numeral) (mk_cnumeral (~i));
+ else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i)));
end;
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Nov 19 10:05:53 2013 +0100
@@ -56,9 +56,6 @@
val long_mk_sum = Arith_Data.long_mk_sum;
val dest_sum = Arith_Data.dest_sum;
-val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
-val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} dummyT;
-
val mk_times = HOLogic.mk_binop @{const_name Groups.times};
fun one_of T = Const(@{const_name Groups.one}, T);
@@ -181,7 +178,7 @@
(*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
val add_0s = @{thms add_0s};
-val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
+val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
(* For post-simplification of the rhs of simproc-generated rules *)
val post_simps =
@@ -194,9 +191,8 @@
val field_post_simps =
post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
-(*Simplify inverse Numeral1, a/Numeral1*)
+(*Simplify inverse Numeral1*)
val inverse_1s = [@{thm inverse_numeral_1}];
-val divide_1s = [@{thm divide_numeral_1}];
(*To perform binary arithmetic. The "left" rewriting handles patterns
created by the Numeral_Simprocs, such as 3 * (5 * x). *)
@@ -217,7 +213,7 @@
@{thms add_neg_numeral_simps}) simps;
(*To evaluate binary negations of coefficients*)
-val minus_simps = [@{thm minus_zero}, @{thm minus_one}, @{thm minus_numeral}, @{thm minus_neg_numeral}];
+val minus_simps = [@{thm minus_zero}, @{thm minus_minus}];
(*To let us treat subtraction as addition*)
val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
@@ -225,16 +221,13 @@
(*To let us treat division as multiplication*)
val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
-(*push the unary minus down*)
-val minus_mult_eq_1_to_2 = @{lemma "- (a::'a::ring) * b = a * - b" by simp};
-
(*to extract again any uncancelled minuses*)
val minus_from_mult_simps =
[@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
(*combine unary minus with numeric literals, however nested within a product*)
val mult_minus_simps =
- [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
+ [@{thm mult_assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}];
val norm_ss1 =
simpset_of (put_simpset num_ss @{context}
@@ -247,7 +240,7 @@
val norm_ss3 =
simpset_of (put_simpset num_ss @{context}
- addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac})
+ addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac minus_mult_commute})
structure CancelNumeralsCommon =
struct
@@ -330,7 +323,7 @@
structure FieldCombineNumeralsData =
struct
type coeff = int * int
- val iszero = (fn (p, q) => p = 0)
+ val iszero = (fn (p, _) => p = 0)
val add = add_frac
val mk_sum = long_mk_sum
val dest_sum = dest_sum
@@ -368,7 +361,7 @@
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac})
+ val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
val eq_reflection = eq_reflection
val is_numeral = can HOLogic.dest_number
end;
@@ -388,7 +381,7 @@
val norm_ss2 =
simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
val norm_ss3 =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac})
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -463,9 +456,9 @@
["((l::'a::field_inverse_zero) * m) / n",
"(l::'a::field_inverse_zero) / (m * n)",
"((numeral v)::'a::field_inverse_zero) / (numeral w)",
- "((numeral v)::'a::field_inverse_zero) / (neg_numeral w)",
- "((neg_numeral v)::'a::field_inverse_zero) / (numeral w)",
- "((neg_numeral v)::'a::field_inverse_zero) / (neg_numeral w)"],
+ "((numeral v)::'a::field_inverse_zero) / (- numeral w)",
+ "((- numeral v)::'a::field_inverse_zero) / (numeral w)",
+ "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"],
DivideCancelNumeralFactor.proc)]
@@ -516,7 +509,7 @@
val find_first = find_first_t []
val trans_tac = trans_tac
val norm_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac})
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac minus_mult_commute})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
val simplify_meta_eq = cancel_simplify_meta_eq
--- a/src/HOL/Transcendental.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Transcendental.thy Tue Nov 19 10:05:53 2013 +0100
@@ -2000,8 +2000,8 @@
apply (subst powr_add, simp, simp)
done
-lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
- unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
+lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
+ unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
apply (case_tac "x = 0", simp, simp)
@@ -2020,11 +2020,17 @@
then show ?thesis by (simp add: assms powr_realpow[symmetric])
qed
-lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n"
- using powr_realpow[of x "numeral n"] by simp
-
-lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n"
- using powr_int[of x "neg_numeral n"] by simp
+lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
+ using powr_realpow [of x 1] by simp
+
+lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
+ by (fact powr_realpow_numeral)
+
+lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
+ using powr_int [of x "- 1"] by simp
+
+lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
+ using powr_int [of x "- numeral n"] by simp
lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
@@ -4047,7 +4053,7 @@
show "sgn x * pi / 2 - arctan x < pi / 2"
using arctan_bounded [of "- x"] assms
unfolding sgn_real_def arctan_minus
- by auto
+ by (auto simp add: algebra_simps)
show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
unfolding sgn_real_def
--- a/src/HOL/Word/Bit_Int.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/Bit_Int.thy Tue Nov 19 10:05:53 2013 +0100
@@ -52,10 +52,10 @@
lemma int_not_simps [simp]:
"NOT (0::int) = -1"
"NOT (1::int) = -2"
- "NOT (-1::int) = 0"
- "NOT (numeral w::int) = neg_numeral (w + Num.One)"
- "NOT (neg_numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
- "NOT (neg_numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
+ "NOT (- 1::int) = 0"
+ "NOT (numeral w::int) = - numeral (w + Num.One)"
+ "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
+ "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
unfolding int_not_def by simp_all
lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
@@ -228,11 +228,11 @@
by (metis bin_rl_simp)
lemma bin_rest_neg_numeral_BitM [simp]:
- "bin_rest (neg_numeral (Num.BitM w)) = neg_numeral w"
+ "bin_rest (- numeral (Num.BitM w)) = - numeral w"
by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
lemma bin_last_neg_numeral_BitM [simp]:
- "bin_last (neg_numeral (Num.BitM w)) = 1"
+ "bin_last (- numeral (Num.BitM w)) = 1"
by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
text {* FIXME: The rule sets below are very large (24 rules for each
@@ -243,26 +243,26 @@
"numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 0"
"numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
"numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 1"
- "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
- "numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 0"
- "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (numeral x AND neg_numeral y) BIT 0"
- "numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (numeral x AND neg_numeral (y + Num.One)) BIT 1"
- "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (neg_numeral x AND numeral y) BIT 0"
- "neg_numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (neg_numeral x AND numeral y) BIT 0"
- "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 0"
- "neg_numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND numeral y) BIT 1"
- "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral x AND neg_numeral y) BIT 0"
- "neg_numeral (Num.Bit0 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral x AND neg_numeral (y + Num.One)) BIT 0"
- "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) AND neg_numeral y) BIT 0"
- "neg_numeral (Num.Bit1 x) AND neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) AND neg_numeral (y + Num.One)) BIT 1"
+ "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
+ "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 0"
+ "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
+ "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 1"
+ "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT 0"
+ "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT 0"
+ "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT 0"
+ "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT 1"
+ "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT 0"
+ "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT 0"
+ "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT 0"
+ "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT 1"
"(1::int) AND numeral (Num.Bit0 y) = 0"
"(1::int) AND numeral (Num.Bit1 y) = 1"
- "(1::int) AND neg_numeral (Num.Bit0 y) = 0"
- "(1::int) AND neg_numeral (Num.Bit1 y) = 1"
+ "(1::int) AND - numeral (Num.Bit0 y) = 0"
+ "(1::int) AND - numeral (Num.Bit1 y) = 1"
"numeral (Num.Bit0 x) AND (1::int) = 0"
"numeral (Num.Bit1 x) AND (1::int) = 1"
- "neg_numeral (Num.Bit0 x) AND (1::int) = 0"
- "neg_numeral (Num.Bit1 x) AND (1::int) = 1"
+ "- numeral (Num.Bit0 x) AND (1::int) = 0"
+ "- numeral (Num.Bit1 x) AND (1::int) = 1"
by (rule bin_rl_eqI, simp, simp)+
lemma int_or_numerals [simp]:
@@ -270,26 +270,26 @@
"numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
"numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 1"
"numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
- "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 0"
- "numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
- "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (numeral x OR neg_numeral y) BIT 1"
- "numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (numeral x OR neg_numeral (y + Num.One)) BIT 1"
- "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (neg_numeral x OR numeral y) BIT 0"
- "neg_numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (neg_numeral x OR numeral y) BIT 1"
- "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
- "neg_numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR numeral y) BIT 1"
- "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral x OR neg_numeral y) BIT 0"
- "neg_numeral (Num.Bit0 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral x OR neg_numeral (y + Num.One)) BIT 1"
- "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) OR neg_numeral y) BIT 1"
- "neg_numeral (Num.Bit1 x) OR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) OR neg_numeral (y + Num.One)) BIT 1"
+ "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 0"
+ "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
+ "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 1"
+ "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
+ "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT 0"
+ "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT 1"
+ "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
+ "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
+ "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT 0"
+ "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT 1"
+ "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT 1"
+ "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT 1"
"(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
"(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
- "(1::int) OR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
- "(1::int) OR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit1 y)"
+ "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
+ "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
"numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
"numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
- "neg_numeral (Num.Bit0 x) OR (1::int) = neg_numeral (Num.BitM x)"
- "neg_numeral (Num.Bit1 x) OR (1::int) = neg_numeral (Num.Bit1 x)"
+ "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
+ "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
by (rule bin_rl_eqI, simp, simp)+
lemma int_xor_numerals [simp]:
@@ -297,26 +297,26 @@
"numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 1"
"numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 1"
"numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 0"
- "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 0"
- "numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 1"
- "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (numeral x XOR neg_numeral y) BIT 1"
- "numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (numeral x XOR neg_numeral (y + Num.One)) BIT 0"
- "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (neg_numeral x XOR numeral y) BIT 0"
- "neg_numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (neg_numeral x XOR numeral y) BIT 1"
- "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 1"
- "neg_numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR numeral y) BIT 0"
- "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral x XOR neg_numeral y) BIT 0"
- "neg_numeral (Num.Bit0 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral x XOR neg_numeral (y + Num.One)) BIT 1"
- "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit0 y) = (neg_numeral (x + Num.One) XOR neg_numeral y) BIT 1"
- "neg_numeral (Num.Bit1 x) XOR neg_numeral (Num.Bit1 y) = (neg_numeral (x + Num.One) XOR neg_numeral (y + Num.One)) BIT 0"
+ "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 0"
+ "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 1"
+ "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 1"
+ "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 0"
+ "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT 0"
+ "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT 1"
+ "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT 1"
+ "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT 0"
+ "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT 0"
+ "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT 1"
+ "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT 1"
+ "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT 0"
"(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
"(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
- "(1::int) XOR neg_numeral (Num.Bit0 y) = neg_numeral (Num.BitM y)"
- "(1::int) XOR neg_numeral (Num.Bit1 y) = neg_numeral (Num.Bit0 (y + Num.One))"
+ "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
+ "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
"numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
"numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
- "neg_numeral (Num.Bit0 x) XOR (1::int) = neg_numeral (Num.BitM x)"
- "neg_numeral (Num.Bit1 x) XOR (1::int) = neg_numeral (Num.Bit0 (x + Num.One))"
+ "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
+ "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
by (rule bin_rl_eqI, simp, simp)+
subsubsection {* Interactions with arithmetic *}
--- a/src/HOL/Word/Bit_Representation.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Tue Nov 19 10:05:53 2013 +0100
@@ -61,21 +61,23 @@
lemma BIT_bin_simps [simp]:
"numeral k BIT 0 = numeral (Num.Bit0 k)"
"numeral k BIT 1 = numeral (Num.Bit1 k)"
- "neg_numeral k BIT 0 = neg_numeral (Num.Bit0 k)"
- "neg_numeral k BIT 1 = neg_numeral (Num.BitM k)"
- unfolding neg_numeral_def numeral.simps numeral_BitM
+ "(- numeral k) BIT 0 = - numeral (Num.Bit0 k)"
+ "(- numeral k) BIT 1 = - numeral (Num.BitM k)"
+ unfolding numeral.simps numeral_BitM
unfolding Bit_def bitval_simps
by (simp_all del: arith_simps add_numeral_special diff_numeral_special)
lemma BIT_special_simps [simp]:
- shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3"
+ shows "0 BIT 0 = 0" and "0 BIT 1 = 1"
+ and "1 BIT 0 = 2" and "1 BIT 1 = 3"
+ and "(- 1) BIT 0 = - 2" and "(- 1) BIT 1 = - 1"
unfolding Bit_def by simp_all
lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
by (subst BIT_eq_iff [symmetric], simp)
-lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
- by (subst BIT_eq_iff [symmetric], simp)
+lemma Bit_eq_m1_iff: "w BIT b = - 1 \<longleftrightarrow> w = - 1 \<and> b = 1"
+ by (cases b) (auto simp add: Bit_def, arith)
lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
by (induct w, simp_all)
@@ -83,8 +85,8 @@
lemma expand_BIT:
"numeral (Num.Bit0 w) = numeral w BIT 0"
"numeral (Num.Bit1 w) = numeral w BIT 1"
- "neg_numeral (Num.Bit0 w) = neg_numeral w BIT 0"
- "neg_numeral (Num.Bit1 w) = neg_numeral (w + Num.One) BIT 1"
+ "- numeral (Num.Bit0 w) = - numeral w BIT 0"
+ "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT 1"
unfolding add_One by (simp_all add: BitM_inc)
lemma bin_last_numeral_simps [simp]:
@@ -94,9 +96,9 @@
"bin_last Numeral1 = 1"
"bin_last (numeral (Num.Bit0 w)) = 0"
"bin_last (numeral (Num.Bit1 w)) = 1"
- "bin_last (neg_numeral (Num.Bit0 w)) = 0"
- "bin_last (neg_numeral (Num.Bit1 w)) = 1"
- unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def)
+ "bin_last (- numeral (Num.Bit0 w)) = 0"
+ "bin_last (- numeral (Num.Bit1 w)) = 1"
+ unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def zmod_zminus1_eq_if)
lemma bin_rest_numeral_simps [simp]:
"bin_rest 0 = 0"
@@ -105,9 +107,9 @@
"bin_rest Numeral1 = 0"
"bin_rest (numeral (Num.Bit0 w)) = numeral w"
"bin_rest (numeral (Num.Bit1 w)) = numeral w"
- "bin_rest (neg_numeral (Num.Bit0 w)) = neg_numeral w"
- "bin_rest (neg_numeral (Num.Bit1 w)) = neg_numeral (w + Num.One)"
- unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def)
+ "bin_rest (- numeral (Num.Bit0 w)) = - numeral w"
+ "bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
+ unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
lemma less_Bits:
"(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
@@ -197,42 +199,45 @@
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT)
-lemma bin_nth_lem [rule_format]:
- "ALL y. bin_nth x = bin_nth y --> x = y"
- apply (induct x rule: bin_induct)
- apply safe
- apply (erule rev_mp)
- apply (induct_tac y rule: bin_induct)
+lemma bin_nth_eq_iff:
+ "bin_nth x = bin_nth y \<longleftrightarrow> x = y"
+proof -
+ have bin_nth_lem [rule_format]: "ALL y. bin_nth x = bin_nth y --> x = y"
+ apply (induct x rule: bin_induct)
apply safe
- apply (drule_tac x=0 in fun_cong, force)
- apply (erule notE, rule ext,
+ apply (erule rev_mp)
+ apply (induct_tac y rule: bin_induct)
+ apply safe
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (erule notE, rule ext,
drule_tac x="Suc x" in fun_cong, force)
- apply (drule_tac x=0 in fun_cong, force)
- apply (erule rev_mp)
- apply (induct_tac y rule: bin_induct)
- apply safe
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (erule rev_mp)
+ apply (induct_tac y rule: bin_induct)
+ apply safe
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (erule notE, rule ext,
+ drule_tac x="Suc x" in fun_cong, force)
+ apply (metis Bit_eq_m1_iff Z bin_last_BIT)
+ apply (case_tac y rule: bin_exhaust)
+ apply clarify
+ apply (erule allE)
+ apply (erule impE)
+ prefer 2
+ apply (erule conjI)
apply (drule_tac x=0 in fun_cong, force)
- apply (erule notE, rule ext,
- drule_tac x="Suc x" in fun_cong, force)
- apply (drule_tac x=0 in fun_cong, force)
- apply (case_tac y rule: bin_exhaust)
- apply clarify
- apply (erule allE)
- apply (erule impE)
- prefer 2
- apply (erule conjI)
- apply (drule_tac x=0 in fun_cong, force)
- apply (rule ext)
- apply (drule_tac x="Suc ?x" in fun_cong, force)
- done
-
-lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"
+ apply (rule ext)
+ apply (drule_tac x="Suc ?x" in fun_cong, force)
+ done
+ show ?thesis
by (auto elim: bin_nth_lem)
+qed
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]]
-lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
- by (auto intro!: bin_nth_lem del: equalityI)
+lemma bin_eq_iff:
+ "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
+ using bin_nth_eq_iff by auto
lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
by (induct n) auto
@@ -276,8 +281,9 @@
lemma bin_sign_simps [simp]:
"bin_sign 0 = 0"
"bin_sign 1 = 0"
+ "bin_sign (- 1) = - 1"
"bin_sign (numeral k) = 0"
- "bin_sign (neg_numeral k) = -1"
+ "bin_sign (- numeral k) = -1"
"bin_sign (w BIT b) = bin_sign w"
unfolding bin_sign_def Bit_def bitval_def
by (simp_all split: bit.split)
@@ -331,18 +337,18 @@
"bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
"bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT 0"
"bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT 1"
- "bintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
- bintrunc n (neg_numeral w) BIT 0"
- "bintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
- bintrunc n (neg_numeral (w + Num.One)) BIT 1"
+ "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
+ bintrunc n (- numeral w) BIT 0"
+ "bintrunc (Suc n) (- numeral (Num.Bit1 w)) =
+ bintrunc n (- numeral (w + Num.One)) BIT 1"
by simp_all
lemma sbintrunc_0_numeral [simp]:
"sbintrunc 0 1 = -1"
"sbintrunc 0 (numeral (Num.Bit0 w)) = 0"
"sbintrunc 0 (numeral (Num.Bit1 w)) = -1"
- "sbintrunc 0 (neg_numeral (Num.Bit0 w)) = 0"
- "sbintrunc 0 (neg_numeral (Num.Bit1 w)) = -1"
+ "sbintrunc 0 (- numeral (Num.Bit0 w)) = 0"
+ "sbintrunc 0 (- numeral (Num.Bit1 w)) = -1"
by simp_all
lemma sbintrunc_Suc_numeral:
@@ -351,10 +357,10 @@
sbintrunc n (numeral w) BIT 0"
"sbintrunc (Suc n) (numeral (Num.Bit1 w)) =
sbintrunc n (numeral w) BIT 1"
- "sbintrunc (Suc n) (neg_numeral (Num.Bit0 w)) =
- sbintrunc n (neg_numeral w) BIT 0"
- "sbintrunc (Suc n) (neg_numeral (Num.Bit1 w)) =
- sbintrunc n (neg_numeral (w + Num.One)) BIT 1"
+ "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) =
+ sbintrunc n (- numeral w) BIT 0"
+ "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) =
+ sbintrunc n (- numeral (w + Num.One)) BIT 1"
by simp_all
lemma bit_bool:
@@ -580,10 +586,10 @@
bintrunc (pred_numeral k) (numeral w) BIT 0"
"bintrunc (numeral k) (numeral (Num.Bit1 w)) =
bintrunc (pred_numeral k) (numeral w) BIT 1"
- "bintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
- bintrunc (pred_numeral k) (neg_numeral w) BIT 0"
- "bintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
- bintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
+ "bintrunc (numeral k) (- numeral (Num.Bit0 w)) =
+ bintrunc (pred_numeral k) (- numeral w) BIT 0"
+ "bintrunc (numeral k) (- numeral (Num.Bit1 w)) =
+ bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
"bintrunc (numeral k) 1 = 1"
by (simp_all add: bintrunc_numeral)
@@ -592,10 +598,10 @@
sbintrunc (pred_numeral k) (numeral w) BIT 0"
"sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
sbintrunc (pred_numeral k) (numeral w) BIT 1"
- "sbintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
- sbintrunc (pred_numeral k) (neg_numeral w) BIT 0"
- "sbintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
- sbintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
+ "sbintrunc (numeral k) (- numeral (Num.Bit0 w)) =
+ sbintrunc (pred_numeral k) (- numeral w) BIT 0"
+ "sbintrunc (numeral k) (- numeral (Num.Bit1 w)) =
+ sbintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
"sbintrunc (numeral k) 1 = 1"
by (simp_all add: sbintrunc_numeral)
--- a/src/HOL/Word/Word.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/Word.thy Tue Nov 19 10:05:53 2013 +0100
@@ -591,24 +591,24 @@
declare word_numeral_alt [symmetric, code_abbrev]
lemma word_neg_numeral_alt:
- "neg_numeral b = word_of_int (neg_numeral b)"
- by (simp only: neg_numeral_def word_numeral_alt wi_hom_neg)
+ "- numeral b = word_of_int (- numeral b)"
+ by (simp only: word_numeral_alt wi_hom_neg)
declare word_neg_numeral_alt [symmetric, code_abbrev]
lemma word_numeral_transfer [transfer_rule]:
"(fun_rel op = pcr_word) numeral numeral"
- "(fun_rel op = pcr_word) neg_numeral neg_numeral"
- unfolding fun_rel_def word.pcr_cr_eq cr_word_def word_numeral_alt word_neg_numeral_alt
- by simp_all
+ "(fun_rel op = pcr_word) (- numeral) (- numeral)"
+ apply (simp_all add: fun_rel_def word.pcr_cr_eq cr_word_def)
+ using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+
lemma uint_bintrunc [simp]:
"uint (numeral bin :: 'a word) =
bintrunc (len_of TYPE ('a :: len0)) (numeral bin)"
unfolding word_numeral_alt by (rule word_ubin.eq_norm)
-lemma uint_bintrunc_neg [simp]: "uint (neg_numeral bin :: 'a word) =
- bintrunc (len_of TYPE ('a :: len0)) (neg_numeral bin)"
+lemma uint_bintrunc_neg [simp]: "uint (- numeral bin :: 'a word) =
+ bintrunc (len_of TYPE ('a :: len0)) (- numeral bin)"
by (simp only: word_neg_numeral_alt word_ubin.eq_norm)
lemma sint_sbintrunc [simp]:
@@ -616,8 +616,8 @@
sbintrunc (len_of TYPE ('a :: len) - 1) (numeral bin)"
by (simp only: word_numeral_alt word_sbin.eq_norm)
-lemma sint_sbintrunc_neg [simp]: "sint (neg_numeral bin :: 'a word) =
- sbintrunc (len_of TYPE ('a :: len) - 1) (neg_numeral bin)"
+lemma sint_sbintrunc_neg [simp]: "sint (- numeral bin :: 'a word) =
+ sbintrunc (len_of TYPE ('a :: len) - 1) (- numeral bin)"
by (simp only: word_neg_numeral_alt word_sbin.eq_norm)
lemma unat_bintrunc [simp]:
@@ -626,8 +626,8 @@
by (simp only: unat_def uint_bintrunc)
lemma unat_bintrunc_neg [simp]:
- "unat (neg_numeral bin :: 'a :: len0 word) =
- nat (bintrunc (len_of TYPE('a)) (neg_numeral bin))"
+ "unat (- numeral bin :: 'a :: len0 word) =
+ nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
by (simp only: unat_def uint_bintrunc_neg)
lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
@@ -678,7 +678,7 @@
by (simp only: int_word_uint)
lemma uint_neg_numeral:
- "uint (neg_numeral b :: 'a :: len0 word) = neg_numeral b mod 2 ^ len_of TYPE('a)"
+ "uint (- numeral b :: 'a :: len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"
unfolding word_neg_numeral_alt
by (simp only: int_word_uint)
@@ -702,13 +702,16 @@
lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1"
unfolding word_1_wi ..
+lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
+ by (simp add: wi_hom_syms)
+
lemma word_of_int_numeral [simp] :
"(word_of_int (numeral bin) :: 'a :: len0 word) = (numeral bin)"
unfolding word_numeral_alt ..
lemma word_of_int_neg_numeral [simp]:
- "(word_of_int (neg_numeral bin) :: 'a :: len0 word) = (neg_numeral bin)"
- unfolding neg_numeral_def word_numeral_alt wi_hom_syms ..
+ "(word_of_int (- numeral bin) :: 'a :: len0 word) = (- numeral bin)"
+ unfolding word_numeral_alt wi_hom_syms ..
lemma word_int_case_wi:
"word_int_case f (word_of_int i :: 'b word) =
@@ -880,8 +883,8 @@
unfolding word_numeral_alt by (rule to_bl_of_bin)
lemma to_bl_neg_numeral [simp]:
- "to_bl (neg_numeral bin::'a::len0 word) =
- bin_to_bl (len_of TYPE('a)) (neg_numeral bin)"
+ "to_bl (- numeral bin::'a::len0 word) =
+ bin_to_bl (len_of TYPE('a)) (- numeral bin)"
unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
@@ -1156,11 +1159,8 @@
lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b
-lemma word_1_no: "(1::'a::len0 word) = Numeral1"
- by (simp add: word_numeral_alt)
-
-lemma word_m1_wi: "-1 = word_of_int -1"
- by (rule word_neg_numeral_alt)
+lemma word_m1_wi: "- 1 = word_of_int (- 1)"
+ using word_neg_numeral_alt [of Num.One] by simp
lemma word_0_bl [simp]: "of_bl [] = 0"
unfolding of_bl_def by simp
@@ -1215,9 +1215,9 @@
unfolding scast_def by simp
lemma sint_n1 [simp] : "sint -1 = -1"
- unfolding word_m1_wi by (simp add: word_sbin.eq_norm)
-
-lemma scast_n1 [simp]: "scast -1 = -1"
+ unfolding word_m1_wi word_sbin.eq_norm by simp
+
+lemma scast_n1 [simp]: "scast (- 1) = - 1"
unfolding scast_def by simp
lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
@@ -1270,8 +1270,8 @@
lemma succ_pred_no [simp]:
"word_succ (numeral w) = numeral w + 1"
"word_pred (numeral w) = numeral w - 1"
- "word_succ (neg_numeral w) = neg_numeral w + 1"
- "word_pred (neg_numeral w) = neg_numeral w - 1"
+ "word_succ (- numeral w) = - numeral w + 1"
+ "word_pred (- numeral w) = - numeral w - 1"
unfolding word_succ_p1 word_pred_m1 by simp_all
lemma word_sp_01 [simp] :
@@ -2151,19 +2151,19 @@
lemma word_no_log_defs [simp]:
"NOT (numeral a) = word_of_int (NOT (numeral a))"
- "NOT (neg_numeral a) = word_of_int (NOT (neg_numeral a))"
+ "NOT (- numeral a) = word_of_int (NOT (- numeral a))"
"numeral a AND numeral b = word_of_int (numeral a AND numeral b)"
- "numeral a AND neg_numeral b = word_of_int (numeral a AND neg_numeral b)"
- "neg_numeral a AND numeral b = word_of_int (neg_numeral a AND numeral b)"
- "neg_numeral a AND neg_numeral b = word_of_int (neg_numeral a AND neg_numeral b)"
+ "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)"
+ "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)"
+ "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)"
"numeral a OR numeral b = word_of_int (numeral a OR numeral b)"
- "numeral a OR neg_numeral b = word_of_int (numeral a OR neg_numeral b)"
- "neg_numeral a OR numeral b = word_of_int (neg_numeral a OR numeral b)"
- "neg_numeral a OR neg_numeral b = word_of_int (neg_numeral a OR neg_numeral b)"
+ "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)"
+ "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)"
+ "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)"
"numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"
- "numeral a XOR neg_numeral b = word_of_int (numeral a XOR neg_numeral b)"
- "neg_numeral a XOR numeral b = word_of_int (neg_numeral a XOR numeral b)"
- "neg_numeral a XOR neg_numeral b = word_of_int (neg_numeral a XOR neg_numeral b)"
+ "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)"
+ "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)"
+ "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"
by (transfer, rule refl)+
text {* Special cases for when one of the arguments equals 1. *}
@@ -2171,17 +2171,17 @@
lemma word_bitwise_1_simps [simp]:
"NOT (1::'a::len0 word) = -2"
"1 AND numeral b = word_of_int (1 AND numeral b)"
- "1 AND neg_numeral b = word_of_int (1 AND neg_numeral b)"
+ "1 AND - numeral b = word_of_int (1 AND - numeral b)"
"numeral a AND 1 = word_of_int (numeral a AND 1)"
- "neg_numeral a AND 1 = word_of_int (neg_numeral a AND 1)"
+ "- numeral a AND 1 = word_of_int (- numeral a AND 1)"
"1 OR numeral b = word_of_int (1 OR numeral b)"
- "1 OR neg_numeral b = word_of_int (1 OR neg_numeral b)"
+ "1 OR - numeral b = word_of_int (1 OR - numeral b)"
"numeral a OR 1 = word_of_int (numeral a OR 1)"
- "neg_numeral a OR 1 = word_of_int (neg_numeral a OR 1)"
+ "- numeral a OR 1 = word_of_int (- numeral a OR 1)"
"1 XOR numeral b = word_of_int (1 XOR numeral b)"
- "1 XOR neg_numeral b = word_of_int (1 XOR neg_numeral b)"
+ "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
"numeral a XOR 1 = word_of_int (numeral a XOR 1)"
- "neg_numeral a XOR 1 = word_of_int (neg_numeral a XOR 1)"
+ "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
by (transfer, simp)+
lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
@@ -2220,8 +2220,8 @@
by transfer (rule refl)
lemma test_bit_neg_numeral [simp]:
- "(neg_numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
- n < len_of TYPE('a) \<and> bin_nth (neg_numeral w) n"
+ "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
+ n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
by transfer (rule refl)
lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
@@ -2398,7 +2398,7 @@
unfolding word_numeral_alt by (rule msb_word_of_int)
lemma word_msb_neg_numeral [simp]:
- "msb (neg_numeral w::'a::len word) = bin_nth (neg_numeral w) (len_of TYPE('a) - 1)"
+ "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
unfolding word_neg_numeral_alt by (rule msb_word_of_int)
lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
@@ -2528,7 +2528,7 @@
unfolding word_lsb_alt test_bit_numeral by simp
lemma word_lsb_neg_numeral [simp]:
- "lsb (neg_numeral bin :: 'a :: len word) = (bin_last (neg_numeral bin) = 1)"
+ "lsb (- numeral bin :: 'a :: len word) = (bin_last (- numeral bin) = 1)"
unfolding word_lsb_alt test_bit_neg_numeral by simp
lemma set_bit_word_of_int:
@@ -2544,8 +2544,8 @@
unfolding word_numeral_alt by (rule set_bit_word_of_int)
lemma word_set_neg_numeral [simp]:
- "set_bit (neg_numeral bin::'a::len0 word) n b =
- word_of_int (bin_sc n (if b then 1 else 0) (neg_numeral bin))"
+ "set_bit (- numeral bin::'a::len0 word) n b =
+ word_of_int (bin_sc n (if b then 1 else 0) (- numeral bin))"
unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
lemma word_set_bit_0 [simp]:
@@ -2612,8 +2612,14 @@
apply clarsimp
apply clarsimp
apply (drule word_gt_0 [THEN iffD1])
- apply (safe intro!: word_eqI bin_nth_lem)
- apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
+ apply (safe intro!: word_eqI)
+ apply (auto simp add: nth_2p_bin)
+ apply (erule notE)
+ apply (simp (no_asm_use) add: uint_word_of_int word_size)
+ apply (subst mod_pos_pos_trivial)
+ apply simp
+ apply (rule power_strict_increasing)
+ apply simp_all
done
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n"
@@ -2670,7 +2676,7 @@
unfolding word_numeral_alt shiftl1_wi by simp
lemma shiftl1_neg_numeral [simp]:
- "shiftl1 (neg_numeral w) = neg_numeral (Num.Bit0 w)"
+ "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
unfolding word_neg_numeral_alt shiftl1_wi by simp
lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
@@ -4638,9 +4644,6 @@
"1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
by unat_arith
-lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
- by (fact word_1_no [symmetric])
-
declare bin_to_bl_def [simp]
ML_file "Tools/word_lib.ML"
--- a/src/HOL/Word/WordBitwise.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Word/WordBitwise.thy Tue Nov 19 10:05:53 2013 +0100
@@ -461,18 +461,18 @@
= True # rev (bin_to_bl n (numeral nm))"
"rev (bin_to_bl (Suc n) (numeral (num.One)))
= True # replicate n False"
- "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm)))
- = False # rev (bin_to_bl n (neg_numeral nm))"
- "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm)))
- = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
- "rev (bin_to_bl (Suc n) (neg_numeral (num.One)))
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm)))
+ = False # rev (bin_to_bl n (- numeral nm))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm)))
+ = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.One)))
= True # replicate n True"
- "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm + num.One)))
- = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
- "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm + num.One)))
- = False # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
- "rev (bin_to_bl (Suc n) (neg_numeral (num.One + num.One)))
- = False # rev (bin_to_bl n (neg_numeral num.One))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One)))
+ = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One)))
+ = False # rev (bin_to_bl n (- numeral (nm + num.One)))"
+ "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One)))
+ = False # rev (bin_to_bl n (- numeral num.One))"
apply (simp_all add: bin_to_bl_def)
apply (simp_all only: bin_to_bl_aux_alt)
apply (simp_all)