(*  Title:      HOL/Nitpick_Examples/Integer_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2012

Examples featuring Nitpick applied to natural numbers and integers.
*)

section ‹Examples Featuring Nitpick Applied to Natural Numbers and Integers›

theory Integer_Nits
imports Main
begin

nitpick_params [verbose, card = 1-5, bits = 1,2,3,4,6,
                sat_solver = MiniSat, max_threads = 1, timeout = 240]

lemma "Suc x = x + 1"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x < Suc x"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x + y ≥ (x::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "y ≠ 0 ==> x + y > (x::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x + y = y + (x::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x > y ==> x - y ≠ (0::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x ≤ y ==> x - y = (0::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x - (0::nat) = x"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "[x ≠ 0; y ≠ 0] ==> x * y ≠ (0::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "0 * y = (0::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "y * 0 = (0::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "[x ≠ 0; y ≠ 0] ==> x * y ≥ (x::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "[x ≠ 0; y ≠ 0] ==> x * y ≥ (y::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x * y div y = (x::nat)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "y ≠ 0 ==> x * y div y = (x::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "5 * 55 < (260::nat)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
nitpick [binary_ints, bits = 9, expect = genuine]
oops

lemma "nat (of_nat n) = n"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x + y ≥ (x::int)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "[x ≥ 0; y ≥ 0] ==> x + y ≥ (0::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "y ≥ 0 ==> x + y ≥ (x::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x ≥ 0 ==> x + y ≥ (y::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x ≥ 0 ==> x + y ≥ (x::int)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "[x ≤ 0; y ≤ 0] ==> x + y ≤ (0::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "y ≠ 0 ==> x + y > (x::int)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "x + y = y + (x::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x > y ==> x - y ≠ (0::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "x ≤ y ==> x - y = (0::int)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "x - (0::int) = x"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "[x ≠ 0; y ≠ 0] ==> x * y ≠ (0::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "0 * y = (0::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "y * 0 = (0::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "[x ≠ 0; y ≠ 0] ==> x * y ≥ (x::int)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "[x ≠ 0; y ≠ 0] ==> x * y ≥ (y::int)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "x * y div y = (x::int)"
nitpick [unary_ints, expect = genuine]
nitpick [binary_ints, expect = genuine]
oops

lemma "y ≠ 0 ==> x * y div y = (x::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, card = 1-4, bits = 1-4, expect = none]
sorry

lemma "(x * y < 0) ⟷ (x > 0 ∧ y < 0) ∨ (x < 0 ∧ y > (0::int))"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

lemma "-5 * 55 > (-260::int)"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
nitpick [binary_ints, bits = 9, expect = genuine]
oops

lemma "nat (of_nat n) = n"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry

datatype tree = Null | Node nat tree tree

primrec labels where
"labels Null = {}" |
"labels (Node x t u) = {x} ∪ labels t ∪ labels u"

lemma "labels (Node x t u) ≠ labels (Node y v w)"
nitpick [expect = potential] (* unfortunate *)
oops

lemma "labels (Node x t u) ≠ {}"
nitpick [expect = none]
oops

lemma "card (labels t) > 0"
nitpick [expect = potential] (* unfortunate *)
oops

lemma "(∑n ∈ labels t. n + 2) ≥ 2"
nitpick [expect = potential] (* unfortunate *)
oops

lemma "t ≠ Null ==> (∑n ∈ labels t. n + 2) ≥ 2"
nitpick [expect = potential] (* unfortunate *)
sorry

lemma "(∑i ∈ labels (Node x t u). f i::nat) = f x + (∑i ∈ labels t. f i) + (∑i ∈ labels u. f i)"
nitpick [expect = potential] (* unfortunate *)
oops

end