src/HOL/ex/Simproc_Tests.thy
 changeset 45463 9a588a835c1e parent 45462 aba629d6cee5 child 45464 5a5a6e6c6789
equal inserted replaced
45462:aba629d6cee5 45463:9a588a835c1e
`   638   next`
`   638   next`
`   639     assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)"`
`   639     assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)"`
`   640       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact`
`   640       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact`
`   641   next`
`   641   next`
`   642     assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"`
`   642     assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"`
`   643       by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact`
`   643       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact`
`   644   next`
`   644   next`
`   645     assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"`
`   645     assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"`
`   646       by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact`
`   646       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact`
`   647   next`
`   647   next`
`   648     assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"`
`   648     assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"`
`   649       by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact`
`   649       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact`
`   650   next`
`   650   next`
`   651     assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"`
`   651     assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"`
`   652     have "(a*(b*c)) div (d*b*(x*a)) = uu"`
`   652     have "(a*(b*c)) div (d*b*(x*a)) = uu"`
`   653       by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact`
`   653       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact`
`   654   next`
`   654   next`
`   655     assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"`
`   655     assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"`
`   656       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact`
`   656       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact`
`   657   next`
`   657   next`
`   658     assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"`
`   658     assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"`
`   667     assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"`
`   667     assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"`
`   668       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact`
`   668       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact`
`   669   }`
`   669   }`
`   670 end`
`   670 end`
`   671 `
`   671 `
`   672 end`
`   672 subsection {* Numeral-cancellation simprocs for type @{typ nat} *}`
`       `
`   673 `
`       `
`   674 notepad begin`
`       `
`   675   fix x y z :: nat`
`       `
`   676   {`
`       `
`   677     assume "3 * x = 4 * y" have "9*x = 12 * y"`
`       `
`   678       by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact`
`       `
`   679   next`
`       `
`   680     assume "3 * x < 4 * y" have "9*x < 12 * y"`
`       `
`   681       by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact`
`       `
`   682   next`
`       `
`   683     assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"`
`       `
`   684       by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact`
`       `
`   685   next`
`       `
`   686     assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"`
`       `
`   687       by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact`
`       `
`   688   next`
`       `
`   689     assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"`
`       `
`   690       by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact`
`       `
`   691   }`
`       `
`   692 end`
`       `
`   693 `
`       `
`   694 end`