Theory Mini_Nits
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 ‹
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>‹(=) 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