# HG changeset patch # User huffman # Date 1320832688 -3600 # Node ID d660c4b9daa6c9bae57d73b2ebe21bc2c60f303a # Parent bf39b07a7a8eec96bbddd83c0209d053e59b48ef add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type s not in this class); test simprocs using most general type classes instead of just int and rat. diff -r bf39b07a7a8e -r d660c4b9daa6 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Wed Nov 09 14:47:38 2011 +1100 +++ b/src/HOL/Numeral_Simprocs.thy Wed Nov 09 10:58:08 2011 +0100 @@ -103,8 +103,8 @@ {* fn phi => Numeral_Simprocs.combine_numerals *} simproc_setup field_combine_numerals - ("(i::'a::{field_inverse_zero, number_ring}) + j" - |"(i::'a::{field_inverse_zero, number_ring}) - j") = + ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j" + |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") = {* fn phi => Numeral_Simprocs.field_combine_numerals *} simproc_setup inteq_cancel_numerals @@ -141,8 +141,8 @@ {* fn phi => Numeral_Simprocs.le_cancel_numerals *} simproc_setup ring_eq_cancel_numeral_factor - ("(l::'a::{idom,number_ring}) * m = n" - |"(l::'a::{idom,number_ring}) = m * n") = + ("(l::'a::{idom,ring_char_0,number_ring}) * m = n" + |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") = {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *} simproc_setup ring_less_cancel_numeral_factor @@ -156,14 +156,14 @@ {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *} simproc_setup int_div_cancel_numeral_factors - ("((l::'a::{semiring_div,number_ring}) * m) div n" - |"(l::'a::{semiring_div,number_ring}) div (m * n)") = + ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n" + |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") = {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *} simproc_setup divide_cancel_numeral_factor - ("((l::'a::{field_inverse_zero,number_ring}) * m) / n" - |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)" - |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") = + ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n" + |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)" + |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") = {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *} simproc_setup ring_eq_cancel_factor diff -r bf39b07a7a8e -r d660c4b9daa6 src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Wed Nov 09 14:47:38 2011 +1100 +++ b/src/HOL/ex/Simproc_Tests.thy Wed Nov 09 10:58:08 2011 +0100 @@ -24,323 +24,305 @@ subsection {* @{text int_combine_numerals} *} -lemma assumes "10 + (2 * l + oo) = uu" - shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "-3 + (i + (j + k)) = y" - shows "(i + j + 12 + (k::int)) - 15 = y" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "7 + (i + (j + k)) = y" - shows "(i + j + 12 + (k::int)) - 5 = y" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "-4 * (u * v) + (2 * x + y) = w" - shows "(2*x - (u*v) + y) - v*3*u = (w::int)" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w" - shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w" - shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w" - shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "Numeral0 * b + (a + - c) = d" - shows "a + -(b+c) + b = (d::int)" -apply (simp only: minus_add_distrib) -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "-2 * b + (a + - c) = d" - shows "a + -(b+c) - b = (d::int)" -apply (simp only: minus_add_distrib) -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz" - shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "-27 + (i + (j + k)) = y" - shows "(i + j + -12 + (k::int)) - 15 = y" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "27 + (i + (j + k)) = y" - shows "(i + j + 12 + (k::int)) - -15 = y" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - -lemma assumes "3 + (i + (j + k)) = y" - shows "(i + j + -12 + (k::int)) - -15 = y" -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact - +notepad begin + fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring" + { + assume "10 + (2 * l + oo) = uu" + have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "-3 + (i + (j + k)) = y" + have "(i + j + 12 + k) - 15 = y" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "7 + (i + (j + k)) = y" + have "(i + j + 12 + k) - 5 = y" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "-4 * (u * v) + (2 * x + y) = w" + have "(2*x - (u*v) + y) - v*3*u = w" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "Numeral0 * (u*v) + (2 * x * u * v + y) = w" + have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "3 * (u * v) + (2 * x * u * v + y) = w" + have "(2*x*u*v + (u*v)*4 + y) - v*u = w" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "-3 * (u * v) + (- (x * u * v) + - y) = w" + have "u*v - (x*u*v + (u*v)*4 + y) = w" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "Numeral0 * b + (a + - c) = d" + have "a + -(b+c) + b = d" + apply (simp only: minus_add_distrib) + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "-2 * b + (a + - c) = d" + have "a + -(b+c) - b = d" + apply (simp only: minus_add_distrib) + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "-7 + (i + (j + (k + (- u + - y)))) = z" + have "(i + j + -2 + k) - (u + 5 + y) = z" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "-27 + (i + (j + k)) = y" + have "(i + j + -12 + k) - 15 = y" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "27 + (i + (j + k)) = y" + have "(i + j + 12 + k) - -15 = y" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + next + assume "3 + (i + (j + k)) = y" + have "(i + j + -12 + k) - -15 = y" + by (tactic {* test [@{simproc int_combine_numerals}] *}) fact + } +end subsection {* @{text inteq_cancel_numerals} *} -lemma assumes "u = Numeral0" shows "2*u = (u::int)" -by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact +notepad begin + fix i j k u vv w y z w' y' z' :: "'a::number_ring" + { + assume "u = Numeral0" have "2*u = u" + by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) - -lemma assumes "i + (j + k) = 3 + (u + y)" - shows "(i + j + 12 + (k::int)) = u + 15 + y" -by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact - -lemma assumes "7 + (j + (i + k)) = y" - shows "(i + j*2 + 12 + (k::int)) = j + 5 + y" -by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact - -lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" - shows "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)" -by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact - + next + assume "i + (j + k) = 3 + (u + y)" + have "(i + j + 12 + k) = u + 15 + y" + by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact + next + assume "7 + (j + (i + k)) = y" + have "(i + j*2 + 12 + k) = j + 5 + y" + by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact + next + assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" + have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv" + by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact + } +end subsection {* @{text intless_cancel_numerals} *} -lemma assumes "y < 2 * b" shows "y - b < (b::int)" -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact - -lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c" -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact - -lemma assumes "i + (j + k) < 8 + (u + y)" - shows "(i + j + -3 + (k::int)) < u + 5 + y" -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact - -lemma assumes "9 + (i + (j + k)) < u + y" - shows "(i + j + 3 + (k::int)) < u + -6 + y" -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact - +notepad begin + fix b c i j k u y :: "'a::{linordered_idom,number_ring}" + { + assume "y < 2 * b" have "y - b < b" + by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact + next + assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c" + by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact + next + assume "i + (j + k) < 8 + (u + y)" + have "(i + j + -3 + k) < u + 5 + y" + by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact + next + assume "9 + (i + (j + k)) < u + y" + have "(i + j + 3 + k) < u + -6 + y" + by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact + } +end subsection {* @{text ring_eq_cancel_numeral_factor} *} -lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - +notepad begin + fix x y :: "'a::{idom,ring_char_0,number_ring}" + { + assume "3*x = 4*y" have "9*x = 12 * y" + by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact + next + assume "-3*x = 4*y" have "-99*x = 132 * y" + by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact + next + assume "111*x = -44*y" have "999*x = -396 * y" + by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact + next + assume "11*x = 9*y" have "-99*x = -81 * y" + by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact + next + assume "2*x = Numeral1*y" have "-2 * x = -1 * y" + by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact + next + assume "2*x = Numeral1*y" have "-2 * x = -y" + by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact + } +end subsection {* @{text int_div_cancel_numeral_factors} *} -lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)" -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact - -lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)" -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact - -lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)" -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact - -lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)" -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact - -lemma assumes "(2*x) div (Numeral1*y) = z" - shows "(-2 * x) div (-1 * (y::int)) = z" -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact - +notepad begin + fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}" + { + assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z" + by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact + next + assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z" + by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact + next + assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z" + by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact + next + assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z" + by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact + next + assume "(2*x) div (Numeral1*y) = z" + have "(-2 * x) div (-1 * y) = z" + by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact + } +end subsection {* @{text ring_less_cancel_numeral_factor} *} -lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - -lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)" -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact - +notepad begin + fix x y :: "'a::{linordered_idom,number_ring}" + { + assume "3*x < 4*y" have "9*x < 12 * y" + by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact + next + assume "-3*x < 4*y" have "-99*x < 132 * y" + by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact + next + assume "111*x < -44*y" have "999*x < -396 * y" + by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact + next + assume "9*y < 11*x" have "-99*x < -81 * y" + by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact + next + assume "Numeral1*y < 2*x" have "-2 * x < -y" + by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact + next + assume "23*y < Numeral1*x" have "-x < -23 * y" + by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact + } +end subsection {* @{text ring_le_cancel_numeral_factor} *} -lemma assumes "3*x \ 4*y" shows "9*x \ 12 * (y::int)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "-3*x \ 4*y" shows "-99*x \ 132 * (y::int)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "111*x \ -44*y" shows "999*x \ -396 * (y::int)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "9*y \ 11*x" shows "-99*x \ -81 * (y::int)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "Numeral1*y \ 2*x" shows "-2 * x \ -1 * (y::int)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "23*y \ Numeral1*x" shows "-x \ -23 * (y::int)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "Numeral1*y \ Numeral0" shows "0 \ (y::rat) * -2" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "3*x \ 4*y" shows "9*x \ 12 * (y::rat)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "-3*x \ 4*y" shows "-99*x \ 132 * (y::rat)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "111*x \ -44*y" shows "999*x \ -396 * (y::rat)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "-1*x \ Numeral1*y" shows "- ((2::rat) * x) \ 2*y" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "9*y \ 11*x" shows "-99*x \ -81 * (y::rat)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "Numeral1*y \ 2*x" shows "-2 * x \ -1 * (y::rat)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - -lemma assumes "23*y \ Numeral1*x" shows "-x \ -23 * (y::rat)" -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact - - -subsection {* @{text ring_eq_cancel_numeral_factor} *} - -lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact - +notepad begin + fix x y :: "'a::{linordered_idom,number_ring}" + { + assume "3*x \ 4*y" have "9*x \ 12 * y" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + next + assume "-3*x \ 4*y" have "-99*x \ 132 * y" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + next + assume "111*x \ -44*y" have "999*x \ -396 * y" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + next + assume "9*y \ 11*x" have "-99*x \ -81 * y" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + next + assume "Numeral1*y \ 2*x" have "-2 * x \ -1 * y" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + next + assume "23*y \ Numeral1*x" have "-x \ -23 * y" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + next + assume "Numeral1*y \ Numeral0" have "0 \ y * -2" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + next + assume "-1*x \ Numeral1*y" have "- (2 * x) \ 2*y" + by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact + } +end subsection {* @{text divide_cancel_numeral_factor} *} -lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z" -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact - -lemma assumes "(-3*x) / (4*y) = z" shows "(-99*x) / (132 * (y::rat)) = z" -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact - -lemma assumes "(111*x) / (-44*y) = z" shows "(999*x) / (-396 * (y::rat)) = z" -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact - -lemma assumes "(11*x) / (9*y) = z" shows "(-99*x) / (-81 * (y::rat)) = z" -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact - -lemma assumes "(2*x) / (Numeral1*y) = z" shows "(-2 * x) / (-1 * (y::rat)) = z" -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact - +notepad begin + fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}" + { + assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" + by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact + next + assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z" + by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact + next + assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z" + by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact + next + assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z" + by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact + next + assume "(2*x) / (Numeral1*y) = z" have "(-2 * x) / (-1 * y) = z" + by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact + } +end subsection {* @{text ring_eq_cancel_factor} *} -lemma assumes "k = 0 \ x = y" shows "x*k = k*(y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - -lemma assumes "k = 0 \ 1 = y" shows "k = k*(y::int)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - -lemma assumes "b = 0 \ a*c = 1" shows "a*(b*c) = (b::int)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - -lemma assumes "a = 0 \ b = 0 \ c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - -lemma assumes "k = 0 \ x = y" shows "x*k = k*(y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - -lemma assumes "k = 0 \ 1 = y" shows "k = k*(y::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - -lemma assumes "b = 0 \ a*c = 1" shows "a*(b*c) = (b::rat)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - -lemma assumes "a = 0 \ b = 0 \ c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)" -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact - +notepad begin + fix a b c d k x y :: "'a::idom" + { + assume "k = 0 \ x = y" have "x*k = k*y" + by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact + next + assume "k = 0 \ 1 = y" have "k = k*y" + by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact + next + assume "b = 0 \ a*c = 1" have "a*(b*c) = b" + by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact + next + assume "a = 0 \ b = 0 \ c = d*x" have "a*(b*c) = d*b*(x*a)" + by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact + next + assume "k = 0 \ x = y" have "x*k = k*y" + by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact + next + assume "k = 0 \ 1 = y" have "k = k*y" + by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact + } +end subsection {* @{text int_div_cancel_factor} *} -lemma assumes "(if k = 0 then 0 else x div y) = uu" - shows "(x*k) div (k*(y::int)) = (uu::int)" -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact - -lemma assumes "(if k = 0 then 0 else 1 div y) = uu" - shows "(k) div (k*(y::int)) = (uu::int)" -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact - -lemma assumes "(if b = 0 then 0 else a * c) = uu" - shows "(a*(b*c)) div ((b::int)) = (uu::int)" -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact - -lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" - shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)" -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact - +notepad begin + fix a b c d k uu x y :: "'a::semiring_div" + { + assume "(if k = 0 then 0 else x div y) = uu" + have "(x*k) div (k*y) = uu" + by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact + next + assume "(if k = 0 then 0 else 1 div y) = uu" + have "(k) div (k*y) = uu" + by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact + next + assume "(if b = 0 then 0 else a * c) = uu" + have "(a*(b*c)) div b = uu" + by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact + next + assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" + have "(a*(b*c)) div (d*b*(x*a)) = uu" + by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact + } +end subsection {* @{text divide_cancel_factor} *} -lemma assumes "(if k = 0 then 0 else x / y) = uu" - shows "(x*k) / (k*(y::rat)) = (uu::rat)" -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact - -lemma assumes "(if k = 0 then 0 else 1 / y) = uu" - shows "(k) / (k*(y::rat)) = (uu::rat)" -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact - -lemma assumes "(if b = 0 then 0 else a * c / 1) = uu" - shows "(a*(b*c)) / ((b::rat)) = (uu::rat)" -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact - -lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" - shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)" -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact +notepad begin + fix a b c d k uu x y :: "'a::field_inverse_zero" + { + assume "(if k = 0 then 0 else x / y) = uu" + have "(x*k) / (k*y) = uu" + by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact + next + assume "(if k = 0 then 0 else 1 / y) = uu" + have "(k) / (k*y) = uu" + by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact + next + assume "(if b = 0 then 0 else a * c / 1) = uu" + have "(a*(b*c)) / b = uu" + by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact + next + assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" + have "(a*(b*c)) / (d*b*(x*a)) = uu" + by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact + } +end lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" oops -- "FIXME: need simproc to cover this case" @@ -348,38 +330,51 @@ subsection {* @{text linordered_ring_less_cancel_factor} *} -lemma assumes "0 < z \ x < y" shows "(0::rat) < z \ x*z < y*z" -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact - -lemma assumes "0 < z \ x < y" shows "(0::rat) < z \ x*z < z*y" -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact - -lemma assumes "0 < z \ x < y" shows "(0::rat) < z \ z*x < y*z" -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact - -lemma assumes "0 < z \ x < y" shows "(0::rat) < z \ z*x < z*y" -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact - +notepad begin + fix x y z :: "'a::linordered_idom" + { + assume "0 < z \ x < y" have "0 < z \ x*z < y*z" + by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact + next + assume "0 < z \ x < y" have "0 < z \ x*z < z*y" + by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact + next + assume "0 < z \ x < y" have "0 < z \ z*x < y*z" + by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact + next + assume "0 < z \ x < y" have "0 < z \ z*x < z*y" + by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact + } +end subsection {* @{text linordered_ring_le_cancel_factor} *} -lemma assumes "0 < z \ x \ y" shows "(0::rat) < z \ x*z \ y*z" -by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact - -lemma assumes "0 < z \ x \ y" shows "(0::rat) < z \ z*x \ z*y" -by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact - +notepad begin + fix x y z :: "'a::linordered_idom" + { + assume "0 < z \ x \ y" have "0 < z \ x*z \ y*z" + by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact + next + assume "0 < z \ x \ y" have "0 < z \ z*x \ z*y" + by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact + } +end subsection {* @{text field_combine_numerals} *} -lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu" -by (tactic {* test [@{simproc field_combine_numerals}] *}) fact - -lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu" -by (tactic {* test [@{simproc field_combine_numerals}] *}) fact - -lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu" -by (tactic {* test [@{simproc field_combine_numerals}] *}) fact +notepad begin + fix x uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}" + { + assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu" + by (tactic {* test [@{simproc field_combine_numerals}] *}) fact + next + assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu" + by (tactic {* test [@{simproc field_combine_numerals}] *}) fact + next + assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu" + by (tactic {* test [@{simproc field_combine_numerals}] *}) fact + } +end lemma "2/3 * (x::rat) + x / 3 = uu" apply (tactic {* test [@{simproc field_combine_numerals}] *})?