Theory Mini_Nits

theory Mini_Nits
imports Main
(*  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_JNI, max_threads = 1,
  total_consts = smart]

ML ‹
val check = Minipick.minipick @{context}
val expect = Minipick.minipick_expect @{context}
val none = expect "none"
val genuine = expect "genuine"
val 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 "(op =) 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 "(ALL 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