(* 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_JNI, 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