src/HOL/ex/Simproc_Tests.thy
changeset 46240 933f35c4e126
parent 45530 0c4853bb77bf
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 11:15:36 2012 +0100
     1.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 16:30:54 2012 +0100
     1.3 @@ -366,6 +366,14 @@
     1.4    next
     1.5      assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
     1.6        by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
     1.7 +  next
     1.8 +    txt "This simproc now uses the simplifier to prove that terms to
     1.9 +      be canceled are positive/negative."
    1.10 +    assume z_pos: "0 < z"
    1.11 +    assume "x < y" have "z*x < z*y"
    1.12 +      by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss
    1.13 +        addsimprocs [@{simproc linordered_ring_less_cancel_factor}]
    1.14 +        addsimps [@{thm z_pos}]) 1) *}) fact
    1.15    }
    1.16  end
    1.17