author huffman Tue, 17 Jan 2012 16:30:54 +0100 changeset 46240 933f35c4e126 parent 46239 fcfb4aa8e6e6 child 46241 1a0b8f529b96
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
 src/HOL/Fact.thy file | annotate | diff | comparison | revisions src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Tools/numeral_simprocs.ML file | annotate | diff | comparison | revisions src/HOL/Transcendental.thy file | annotate | diff | comparison | revisions src/HOL/Word/Bool_List_Representation.thy file | annotate | diff | comparison | revisions src/HOL/ex/Simproc_Tests.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Fact.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Fact.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -255,8 +255,6 @@
fact m < fact ((m + 1) + k)"
apply (induct k rule: int_ge_induct)
-  apply (subst mult_less_cancel_right1)
-  apply (insert fact_gt_zero_int [of m], arith)
apply (subst (2) fact_reduce_int)
apply (erule order_less_le_trans)```
```--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -723,8 +723,6 @@
using t(1,2) m(2)[rule_format, OF tw] w0
apply (simp only: )
apply auto
-        apply (rule mult_mono, simp_all add: norm_ge_zero)+
-        apply (simp add: zero_le_mult_iff zero_le_power)
done
with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"```
```--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 17 16:30:54 2012 +0100
@@ -461,8 +461,9 @@
val zero = Const(@{const_name Groups.zero}, T);
val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
val pos = less \$ zero \$ t and neg = less \$ t \$ zero
+      val thy = Proof_Context.theory_of (Simplifier.the_context ss)
fun prove p =
-        Option.map Eq_True_elim (Lin_Arith.simproc ss p)
+        SOME (Eq_True_elim (Simplifier.asm_rewrite ss (Thm.cterm_of thy p)))
handle THM _ => NONE
in case prove pos of
SOME th => SOME(th RS pos_th)```
```--- a/src/HOL/Transcendental.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Transcendental.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -1478,9 +1478,6 @@
thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
qed

-lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
-by simp
-
lemma real_mult_inverse_cancel:
"[|(0::real) < x; 0 < x1; x1 * y < x * u |]
==> inverse x * y < inverse x1 * u"
@@ -1516,11 +1513,7 @@
unfolding One_nat_def
del: fact_Suc)
-apply (rule real_mult_inverse_cancel2)
-apply (simp del: fact_Suc)
-apply (simp del: fact_Suc)
-apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
-apply (subst fact_lemma)
+apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
apply (simp only: real_of_nat_mult)
apply (rule mult_strict_mono, force)```
```--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -318,9 +318,7 @@
apply clarsimp
apply clarsimp
apply safe
-  apply (drule meta_spec, erule xtr8 [rotated],
-         simp add: numeral_simps algebra_simps BIT_simps
+  apply (drule meta_spec, erule xtr8 [rotated], simp add: Bit_def)+
done

lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"```
```--- a/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -366,6 +366,14 @@
next
assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
+  next
+    txt "This simproc now uses the simplifier to prove that terms to
+      be canceled are positive/negative."
+    assume z_pos: "0 < z"
+    assume "x < y" have "z*x < z*y"
+      by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss