--- a/src/HOL/Divides.thy Wed Nov 16 23:09:46 2011 +0100
+++ b/src/HOL/Divides.thy Thu Nov 17 05:27:45 2011 +0100
@@ -1663,13 +1663,22 @@
text {*Simplify expresions in which div and mod combine numerical constants*}
-lemma divmod_int_relI:
- "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
- \<Longrightarrow> divmod_int_rel a b (q, r)"
- unfolding divmod_int_rel_def by simp
-
-lemmas divmod_int_rel_div_eq = divmod_int_relI [THEN divmod_int_rel_div, THEN eq_reflection]
-lemmas divmod_int_rel_mod_eq = divmod_int_relI [THEN divmod_int_rel_mod, THEN eq_reflection]
+lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
+ by (rule divmod_int_rel_div [of a b q r],
+ simp add: divmod_int_rel_def, simp)
+
+lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
+ by (rule divmod_int_rel_div [of a b q r],
+ simp add: divmod_int_rel_def, simp)
+
+lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
+ by (rule divmod_int_rel_mod [of a b q r],
+ simp add: divmod_int_rel_def, simp)
+
+lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
+ by (rule divmod_int_rel_mod [of a b q r],
+ simp add: divmod_int_rel_def, simp)
+
lemmas arithmetic_simps =
arith_simps
add_special
@@ -1683,12 +1692,16 @@
(* simprocs adapted from HOL/ex/Binary.thy *)
ML {*
local
- val mk_number = HOLogic.mk_number HOLogic.intT;
- fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $
- (@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ u $ mk_number k) $
- mk_number l;
- fun prove ctxt prop = Goal.prove ctxt [] [] prop
- (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));
+ val mk_number = HOLogic.mk_number HOLogic.intT
+ val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
+ val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}
+ 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_0_eq_0}, @{thm numeral_1_eq_1}]
+ fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
+ (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps simps))));
fun binary_proc proc ss ct =
(case Thm.term_of ct of
_ $ t $ u =>
@@ -1697,18 +1710,23 @@
| NONE => NONE)
| _ => NONE);
in
- fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
- if n = 0 then NONE
- else let val (k, l) = Integer.div_mod m n;
- in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);
+ fun divmod_proc posrule negrule =
+ binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
+ if b = 0 then NONE else let
+ val (q, r) = pairself mk_number (Integer.div_mod a b)
+ val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
+ val (goal2, goal3, rule) = if b > 0
+ then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
+ else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
+ in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
end
*}
simproc_setup binary_int_div ("number_of m div number_of n :: int") =
- {* K (divmod_proc (@{thm divmod_int_rel_div_eq})) *}
+ {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
- {* K (divmod_proc (@{thm divmod_int_rel_mod_eq})) *}
+ {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
lemmas posDivAlg_eqn_number_of [simp] =
posDivAlg_eqn [of "number_of v" "number_of w", standard]
--- a/src/HOL/Word/Bit_Int.thy Wed Nov 16 23:09:46 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy Thu Nov 17 05:27:45 2011 +0100
@@ -657,7 +657,7 @@
lemma bin_split_num:
"!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
apply (induct n, clarsimp)
- apply (simp add: bin_rest_div zdiv_zmult2_eq)
+ apply (simp add: bin_rest_def zdiv_zmult2_eq)
apply (case_tac b rule: bin_exhaust)
apply simp
apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def
--- a/src/HOL/Word/Bit_Representation.thy Wed Nov 16 23:09:46 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Thu Nov 17 05:27:45 2011 +0100
@@ -227,26 +227,8 @@
"bin_rest -1 = -1"
by (simp_all add: bin_last_def bin_rest_def)
-lemma bin_last_mod:
- "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
- apply (case_tac w rule: bin_exhaust)
- apply (case_tac b)
- apply auto
- done
-
-lemma bin_rest_div:
- "bin_rest w = w div 2"
- apply (case_tac w rule: bin_exhaust)
- apply (rule trans)
- apply clarsimp
- apply (rule refl)
- apply (drule trans)
- apply (rule Bit_def)
- apply (simp add: bitval_def z1pdiv2 split: bit.split)
- done
-
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
- unfolding bin_rest_div [symmetric] by auto
+ unfolding bin_rest_def [symmetric] by auto
lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
using Bit_div2 [where b="(0::bit)"] by simp
@@ -358,7 +340,7 @@
lemma bintrunc_mod2p:
"!!w. bintrunc n w = (w mod 2 ^ n :: int)"
apply (induct n, clarsimp)
- apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq
+ apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq
cong: number_of_False_cong)
done
@@ -367,10 +349,10 @@
apply (induct n)
apply clarsimp
apply (subst mod_add_left_eq)
- apply (simp add: bin_last_mod)
+ apply (simp add: bin_last_def)
apply (simp add: number_of_eq)
apply clarsimp
- apply (simp add: bin_last_mod bin_rest_div Bit_def
+ apply (simp add: bin_last_def bin_rest_def Bit_def
cong: number_of_False_cong)
apply (clarsimp simp: mod_mult_mult1 [symmetric]
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
--- a/src/HOL/Word/Misc_Numeric.thy Wed Nov 16 23:09:46 2011 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy Thu Nov 17 05:27:45 2011 +0100
@@ -247,58 +247,6 @@
apply (simp add: zmde ring_distribs)
done
-(** Rep_Integ **)
-lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"
- unfolding equiv_def refl_on_def quotient_def Image_def by auto
-
-lemmas Rep_Integ_ne = Integ.Rep_Integ
- [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]
-
-lemmas riq = Integ.Rep_Integ [simplified Integ_def]
-lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard]
-lemmas Rep_Integ_equiv = quotient_eq_iff
- [OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard]
-lemmas Rep_Integ_same =
- Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard]
-
-lemma RI_int: "(a, 0) : Rep_Integ (int a)"
- unfolding int_def by auto
-
-lemmas RI_intrel [simp] = UNIV_I [THEN quotientI,
- THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard]
-
-lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ (- x)"
- apply (rule_tac z=x in eq_Abs_Integ)
- apply (clarsimp simp: minus)
- done
-
-lemma RI_add:
- "(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==>
- (a + c, b + d) : Rep_Integ (x + y)"
- apply (rule_tac z=x in eq_Abs_Integ)
- apply (rule_tac z=y in eq_Abs_Integ)
- apply (clarsimp simp: add)
- done
-
-lemma mem_same: "a : S ==> a = b ==> b : S"
- by fast
-
-(* two alternative proofs of this *)
-lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
- apply (unfold diff_minus)
- apply (rule mem_same)
- apply (rule RI_minus RI_add RI_int)+
- apply simp
- done
-
-lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a - int b = x)"
- apply safe
- apply (rule Rep_Integ_same)
- prefer 2
- apply (erule asm_rl)
- apply (rule RI_eq_diff')+
- done
-
lemma mod_power_lem:
"a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
apply clarsimp
--- a/src/HOL/Word/Word.thy Wed Nov 16 23:09:46 2011 +0100
+++ b/src/HOL/Word/Word.thy Thu Nov 17 05:27:45 2011 +0100
@@ -1769,16 +1769,8 @@
lemma word_of_int: "of_int = word_of_int"
apply (rule ext)
- apply (unfold of_int_def)
- apply (rule the_elemI)
- apply safe
- apply (simp_all add: word_of_nat word_of_int_homs)
- defer
- apply (rule Rep_Integ_ne [THEN nonemptyE])
- apply (rule bexI)
- prefer 2
- apply assumption
- apply (auto simp add: RI_eq_diff)
+ apply (case_tac x rule: int_diff_cases)
+ apply (simp add: word_of_nat word_of_int_sub_hom)
done
lemma word_of_int_nat:
@@ -2436,7 +2428,7 @@
done
lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
- unfolding word_lsb_def bin_last_mod by auto
+ unfolding word_lsb_def bin_last_def by auto
lemma word_msb_sint: "msb w = (sint w < 0)"
unfolding word_msb_def
@@ -2831,7 +2823,7 @@
done
lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
- apply (unfold shiftr1_def bin_rest_div)
+ apply (unfold shiftr1_def bin_rest_def)
apply (rule word_uint.Abs_inverse)
apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
apply (rule xtr7)
@@ -2841,7 +2833,7 @@
done
lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
- apply (unfold sshiftr1_def bin_rest_div [symmetric])
+ apply (unfold sshiftr1_def bin_rest_def [symmetric])
apply (simp add: word_sbin.eq_norm)
apply (rule trans)
defer
--- a/src/HOL/ex/Simproc_Tests.thy Wed Nov 16 23:09:46 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy Thu Nov 17 05:27:45 2011 +0100
@@ -420,9 +420,11 @@
assume "4*k = u" have "k + 3*k = u"
by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
next
+ (* FIXME "Suc (i + 3) \<equiv> i + 4" *)
assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
next
+ (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *)
assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
next
@@ -712,4 +714,43 @@
}
end
+subsection {* Integer numeral div/mod simprocs *}
+
+notepad begin
+ have "(10::int) div 3 = 3"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "(10::int) mod 3 = 1"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "(10::int) div -3 = -4"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "(10::int) mod -3 = -2"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "(-10::int) div 3 = -4"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "(-10::int) mod 3 = 2"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "(-10::int) div -3 = 3"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "(-10::int) mod -3 = -1"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "(8452::int) mod 3 = 1"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "(59485::int) div 434 = 137"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "(1000006::int) mod 10 = 6"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "10000000 div 2 = (5000000::int)"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "10000001 mod 2 = (1::int)"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "10000055 div 32 = (312501::int)"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "10000055 mod 32 = (23::int)"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
+ have "100094 div 144 = (695::int)"
+ by (tactic {* test [@{simproc binary_int_div}] *})
+ have "100094 mod 144 = (14::int)"
+ by (tactic {* test [@{simproc binary_int_mod}] *})
end
+
+end