factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
authorhuffman
Tue Jan 17 16:30:54 2012 +0100 (2012-01-17)
changeset 46240933f35c4e126
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
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Transcendental.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/ex/Simproc_Tests.thy
     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.6    apply (simp add: fact_plus_one_int)
     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.10    apply (auto simp add: add_ac)
    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.15  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
    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.9 -         cong add: number_of_False_cong)+
    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.13 +        addsimprocs [@{simproc linordered_ring_less_cancel_factor}]
    6.14 +        addsimps [@{thm z_pos}]) 1) *}) fact
    6.15    }
    6.16  end
    6.17