Quelle  Mini_Nits.thy

(*  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 ‹
 val check = Minipick.minipick 🍋
 val expect = Minipick.minipick_expect 🍋
 val none = expect "none"
 val genuine = expect "genuine"
 val unknown = expect "unknown"
 ›

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

end