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

Examples featuring Minipick, the minimalistic version of Nitpick.
*)

section ‹Examples Featuring Minipick, the Minimalistic Version of Nitpick›

theory Mini_Nits
imports Main
begin

ML_file ‹minipick.ML›

nitpick_params [verbose, sat_solver = MiniSat, max_threads = 1, total_consts = smart]

ML ‹
  check = Minipick.minipick context
  expect = Minipick.minipick_expect context
  none = expect "none"
  genuine = expect "genuine"
  unknown = expect "unknown"
 ›

ML ‹genuine 1 prop‹x = Not››
ML ‹none 1 prop‹∃x. x = Not››
ML ‹none 1 prop‹¬ False››
ML ‹genuine 1 prop‹¬ True››
ML ‹none 1 prop‹¬ ¬ b ⟷ b››
ML ‹none 1 prop‹True››
ML ‹genuine 1 prop‹False››
ML ‹genuine 1 prop‹True ⟷ False››
ML ‹none 1 prop‹True ⟷ ¬ False››
ML ‹none 4 prop‹∀x. x = x››
ML ‹none 4 prop‹∃x. x = x››
ML ‹none 1 prop‹∀x. x = y››
ML ‹genuine 2 prop‹∀x. x = y››
ML ‹none 2 prop‹∃x. x = y››
ML ‹none 2 prop‹∀x::'a × 'a. x = x››
ML ‹none 2 prop‹∃x::'a × 'a. x = y››
ML ‹genuine 2 prop‹∀x::'a × 'a. x = y››
ML ‹none 2 prop‹∃x::'a × 'a. x = y››
ML ‹none 1 prop‹All = Ex››
ML ‹genuine 2 prop‹All = Ex››
ML ‹none 1 prop‹All P = Ex P››
ML ‹genuine 2 prop‹All P = Ex P››
ML ‹none 4 prop‹x = y ⟶ P x = P y››
ML ‹none 4 prop‹(x::'a × 'a) = y ⟶ P x = P y››
ML ‹none 2 prop‹(x::'a × 'a) = y ⟶ P x y = P y x››
ML ‹none 4 prop‹∃x::'a × 'a. x = y ⟶ P x = P y››
ML ‹none 2 prop‹(x::'a → 'a) = y ⟶ P x = P y››
ML ‹none 2 prop‹∃x::'a → 'a. x = y ⟶ P x = P y››
ML ‹genuine 1 prop‹(=) X = Ex››
ML ‹none 2 prop‹∀x::'a → 'a. x = x››
ML ‹none 1 prop‹x = y››
ML ‹genuine 1 prop‹x ⟷ y››
ML ‹genuine 2 prop‹x = y››
ML ‹genuine 1 prop‹X ⊆ Y››
ML ‹none 1 prop‹P ∧ Q ⟷ Q ∧ P››
ML ‹none 1 prop‹P ∧ Q ⟶ P››
ML ‹none 1 prop‹P ∨ Q ⟷ Q ∨ P››
ML ‹genuine 1 prop‹P ∨ Q ⟶ P››
ML ‹none 1 prop‹(P ⟶ Q) ⟷ (¬ P ∨ Q)››
ML ‹none 4 prop‹{a} = {a, a}››
ML ‹genuine 2 prop‹{a} = {a, b}››
ML ‹genuine 1 prop‹{a} ≠ {a, b}››
ML ‹none 4 prop‹{}⁺ = {}››
ML ‹none 4 prop‹UNIV⁺ = UNIV››
ML ‹none 4 prop‹(UNIV :: ('a × 'b) set) - {} = UNIV››
ML ‹none 4 prop‹{} - (UNIV :: ('a × 'b) set) = {}››
ML ‹none 1 prop‹{(a, b), (b, c)}⁺ = {(a, b), (a, c), (b, c)}››
ML ‹genuine 2 prop‹{(a, b), (b, c)}⁺ = {(a, b), (a, c), (b, c)}››
ML ‹none 4 prop‹a ≠ c ==> {(a, b), (b, c)}⁺ = {(a, b), (a, c), (b, c)}››
ML ‹none 4 prop‹A ∪ B = {x. x ∈ A ∨ x ∈ B}››
ML ‹none 4 prop‹A ∩ B = {x. x ∈ A ∧ x ∈ B}››
ML ‹none 4 prop‹A - B = (λx. A x ∧ ¬ B x)››
ML ‹none 4 prop‹∃a b. (a, b) = (b, a)››
ML ‹genuine 2 prop‹(a, b) = (b, a)››
ML ‹genuine 2 prop‹(a, b) ≠ (b, a)››
ML ‹none 4 prop‹∃a b::'a × 'a. (a, b) = (b, a)››
ML ‹genuine 2 prop‹(a::'a × 'a, b) = (b, a)››
ML ‹none 4 prop‹∃a b::'a × 'a × 'a. (a, b) = (b, a)››
ML ‹genuine 2 prop‹(a::'a × 'a × 'a, b) ≠ (b, a)››
ML ‹none 4 prop‹∃a b::'a → 'a. (a, b) = (b, a)››
ML ‹genuine 1 prop‹(a::'a → 'a, b) ≠ (b, a)››
ML ‹none 4 prop‹fst (a, b) = a››
ML ‹none 1 prop‹fst (a, b) = b››
ML ‹genuine 2 prop‹fst (a, b) = b››
ML ‹genuine 2 prop‹fst (a, b) ≠ b››
ML ‹genuine 2 prop‹f ((x, z), y) = (x, z)››
ML ‹none 2 prop‹(∀x. f x = fst x) ⟶ f ((x, z), y) = (x, z)››
ML ‹none 4 prop‹snd (a, b) = b››
ML ‹none 1 prop‹snd (a, b) = a››
ML ‹genuine 2 prop‹snd (a, b) = a››
ML ‹genuine 2 prop‹snd (a, b) ≠ a››
ML ‹genuine 1 prop‹P››
ML ‹genuine 1 prop‹(λx. P) a››
ML ‹genuine 1 prop‹(λx y z. P y x z) a b c››
ML ‹none 4 prop‹∃f. f = (λx. x) ∧ f y = y››
ML ‹genuine 1 prop‹∃f. f p ≠ p ∧ (∀a b. f (a, b) = (a, b))››
ML ‹none 2 prop‹∃f. ∀a b. f (a, b) = (a, b)››
ML ‹none 3 prop‹f = (λa b. (b, a)) ⟶ f x y = (y, x)››
ML ‹genuine 2 prop‹f = (λa b. (b, a)) ⟶ f x y = (x, y)››
ML ‹none 4 prop‹f = (λx. f x)››
ML ‹none 4 prop‹f = (λx. f x::'a → bool)››
ML ‹none 4 prop‹f = (λx y. f x y)››
ML ‹none 4 prop‹f = (λx y. f x y::'a → bool)››

end