author huffman Tue Jan 17 16:30:54 2012 +0100 (2012-01-17) 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 | revisions src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | revisions src/HOL/Tools/numeral_simprocs.ML file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions src/HOL/Word/Bool_List_Representation.thy file | annotate | diff | revisions src/HOL/ex/Simproc_Tests.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Fact.thy	Tue Jan 17 11:15:36 2012 +0100
1.2 +++ b/src/HOL/Fact.thy	Tue Jan 17 16:30:54 2012 +0100
1.3 @@ -255,8 +255,6 @@
1.4      fact m < fact ((m + 1) + k)"
1.5    apply (induct k rule: int_ge_induct)
1.7 -  apply (subst mult_less_cancel_right1)
1.8 -  apply (insert fact_gt_zero_int [of m], arith)
1.9    apply (subst (2) fact_reduce_int)
1.11    apply (erule order_less_le_trans)
```
```     2.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 11:15:36 2012 +0100
2.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 16:30:54 2012 +0100
2.3 @@ -723,8 +723,6 @@
2.4          using t(1,2) m(2)[rule_format, OF tw] w0
2.5          apply (simp only: )
2.6          apply auto
2.7 -        apply (rule mult_mono, simp_all add: norm_ge_zero)+
2.8 -        apply (simp add: zero_le_mult_iff zero_le_power)
2.9          done
2.10        with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
2.11        from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
```
```     3.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 17 11:15:36 2012 +0100
3.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 17 16:30:54 2012 +0100
3.3 @@ -461,8 +461,9 @@
3.4        val zero = Const(@{const_name Groups.zero}, T);
3.5        val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
3.6        val pos = less \$ zero \$ t and neg = less \$ t \$ zero
3.7 +      val thy = Proof_Context.theory_of (Simplifier.the_context ss)
3.8        fun prove p =
3.9 -        Option.map Eq_True_elim (Lin_Arith.simproc ss p)
3.10 +        SOME (Eq_True_elim (Simplifier.asm_rewrite ss (Thm.cterm_of thy p)))
3.11          handle THM _ => NONE
3.12      in case prove pos of
3.13           SOME th => SOME(th RS pos_th)
```
```     4.1 --- a/src/HOL/Transcendental.thy	Tue Jan 17 11:15:36 2012 +0100
4.2 +++ b/src/HOL/Transcendental.thy	Tue Jan 17 16:30:54 2012 +0100
4.3 @@ -1478,9 +1478,6 @@
4.4    thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
4.5  qed
4.6
4.7 -lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
4.8 -by simp
4.9 -
4.10  lemma real_mult_inverse_cancel:
4.11       "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
4.12        ==> inverse x * y < inverse x1 * u"
4.13 @@ -1516,11 +1513,7 @@
4.14  unfolding One_nat_def
4.16              del: fact_Suc)
4.17 -apply (rule real_mult_inverse_cancel2)
4.18 -apply (simp del: fact_Suc)
4.19 -apply (simp del: fact_Suc)
4.20 -apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
4.21 -apply (subst fact_lemma)
4.22 +apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
4.23  apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
4.24  apply (simp only: real_of_nat_mult)
4.25  apply (rule mult_strict_mono, force)
```
```     5.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Tue Jan 17 11:15:36 2012 +0100
5.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Jan 17 16:30:54 2012 +0100
5.3 @@ -318,9 +318,7 @@
5.4     apply clarsimp
5.5    apply clarsimp
5.6    apply safe
5.7 -  apply (drule meta_spec, erule xtr8 [rotated],
5.8 -         simp add: numeral_simps algebra_simps BIT_simps
5.10 +  apply (drule meta_spec, erule xtr8 [rotated], simp add: Bit_def)+
5.11    done
5.12
5.13  lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
```
```     6.1 --- a/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 11:15:36 2012 +0100
6.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 16:30:54 2012 +0100
6.3 @@ -366,6 +366,14 @@
6.4    next
6.5      assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
6.6        by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
6.7 +  next
6.8 +    txt "This simproc now uses the simplifier to prove that terms to
6.9 +      be canceled are positive/negative."
6.10 +    assume z_pos: "0 < z"
6.11 +    assume "x < y" have "z*x < z*y"
6.12 +      by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss
6.14 +        addsimps [@{thm z_pos}]) 1) *}) fact
6.15    }
6.16  end
6.17
```