1534 |
1534 |
1535 ML_file "Tools/nat_arith.ML" |
1535 ML_file "Tools/nat_arith.ML" |
1536 |
1536 |
1537 simproc_setup nateq_cancel_sums |
1537 simproc_setup nateq_cancel_sums |
1538 ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") = |
1538 ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") = |
1539 {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *} |
1539 {* fn phi => try o Nat_Arith.cancel_eq_conv *} |
1540 |
1540 |
1541 simproc_setup natless_cancel_sums |
1541 simproc_setup natless_cancel_sums |
1542 ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") = |
1542 ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") = |
1543 {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *} |
1543 {* fn phi => try o Nat_Arith.cancel_less_conv *} |
1544 |
1544 |
1545 simproc_setup natle_cancel_sums |
1545 simproc_setup natle_cancel_sums |
1546 ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") = |
1546 ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") = |
1547 {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *} |
1547 {* fn phi => try o Nat_Arith.cancel_le_conv *} |
1548 |
1548 |
1549 simproc_setup natdiff_cancel_sums |
1549 simproc_setup natdiff_cancel_sums |
1550 ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") = |
1550 ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") = |
1551 {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *} |
1551 {* fn phi => try o Nat_Arith.cancel_diff_conv *} |
1552 |
1552 |
1553 ML_file "Tools/lin_arith.ML" |
1553 ML_file "Tools/lin_arith.ML" |
1554 setup {* Lin_Arith.global_setup *} |
1554 setup {* Lin_Arith.global_setup *} |
1555 declaration {* K Lin_Arith.setup *} |
1555 declaration {* K Lin_Arith.setup *} |
1556 |
1556 |